no goals
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
⊢ minpoly A 1 = X - 1
simpa only [RingHom.map_one, C_1, sub_eq_add_neg] using eq_X_sub_C B (1 : A)