no goals
A : Type u_2
B✝ : Type ?u.356948
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_1
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
⊢ minpoly A (x - ↑(algebraMap A B) a) = Polynomial.comp (minpoly A x) (X + ↑C a)
simpa [sub_eq_add_neg] using add_algebraMap hx (-a)