feat(field_theory/minpoly): add minpoly_add_algebra_map and minpoly_s…

…ub_algebra_map (#12357)

We add minpoly_add_algebra_map and minpoly_sub_algebra_map: the minimal polynomial of x ± a.

From flt-regular

src/data/polynomial/ring_division.lean

@@ -571,6 +571,19 @@ lemma leading_coeff_comp (hq : nat_degree q ≠ 0) : leading_coeff (p.comp q) =
   leading_coeff p * leading_coeff q ^ nat_degree p :=
 by rw [← coeff_comp_degree_mul_degree hq, ← nat_degree_comp]; refl
 
+lemma monic.comp (hp : p.monic) (hq : q.monic) (h : q.nat_degree ≠ 0) : (p.comp q).monic :=
+by rw [monic.def, leading_coeff_comp h, monic.def.1 hp, monic.def.1 hq, one_pow, one_mul]
+
+lemma monic.comp_X_add_C (hp : p.monic) (r : R) : (p.comp (X + C r)).monic :=
+begin
+  refine hp.comp (monic_X_add_C _) (λ ha, _),
+  rw [nat_degree_X_add_C] at ha,
+  exact one_ne_zero ha
+end
+
+lemma monic.comp_X_sub_C (hp : p.monic) (r : R) : (p.comp (X - C r)).monic :=
+by simpa using hp.comp_X_add_C (-r)
+
 lemma units_coeff_zero_smul (c : R[X]ˣ) (p : R[X]) :
   (c : R[X]).coeff 0 • p = c * p :=
 by rw [←polynomial.C_mul', ←polynomial.eq_C_of_degree_eq_zero (degree_coe_units c)]

src/field_theory/minpoly.lean

@@ -359,6 +359,27 @@ minpoly.unique _ _ (minpoly.monic hx)
     (is_scalar_tower.aeval_eq_zero_of_aeval_algebra_map_eq_zero K S T hST
       (h ▸ root_q : polynomial.aeval (algebra_map S T x) q = 0)))
 
+lemma minpoly_add_algebra_map {B : Type*} [comm_ring B] [algebra A B] {x : B}
+  (hx : is_integral A x) (a : A) :
+  minpoly A (x + (algebra_map A B a)) = (minpoly A x).comp (X - C a) :=
+begin
+  refine (minpoly.unique _ _ ((minpoly.monic hx).comp_X_sub_C _) _ (λ q qmo hq, _)).symm,
+  { simp [aeval_comp] },
+  { have : (polynomial.aeval x) (q.comp (X + C a)) = 0 := by simpa [aeval_comp] using hq,
+    have H := minpoly.min A x (qmo.comp_X_add_C _) this,
+    rw [degree_eq_nat_degree qmo.ne_zero, degree_eq_nat_degree
+      ((minpoly.monic hx).comp_X_sub_C _).ne_zero, with_bot.coe_le_coe, nat_degree_comp,
+      nat_degree_X_sub_C, mul_one],
+    rwa [degree_eq_nat_degree (minpoly.ne_zero hx), degree_eq_nat_degree
+      (qmo.comp_X_add_C _).ne_zero, with_bot.coe_le_coe, nat_degree_comp,
+      nat_degree_X_add_C, mul_one] at H }
+end
+
+lemma minpoly_sub_algebra_map {B : Type*} [comm_ring B] [algebra A B] {x : B}
+  (hx : is_integral A x) (a : A) :
+  minpoly A (x - (algebra_map A B a)) = (minpoly A x).comp (X + C a) :=
+by simpa [sub_eq_add_neg] using minpoly_add_algebra_map hx (-a)
+
 section gcd_domain
 
 /-- For GCD domains, the minimal polynomial over the ring is the same as the minimal polynomial