add_algebraMap — Mathlib

English

Let A be a field and B an A-algebra. For any x ∈ B and a ∈ A, the minimal polynomial of x + algebraMap_A_B(a) over A equals the composition of the minimal polynomial of x with the translation X ↦ X − C a, i.e. minpoly_A(x + algebraMap_A_B(a)) = (minpoly_A x) ∘ (X − C a).

Русский

Пусть A — поле, B — A-алгебра. Для любых x ∈ B и a ∈ A минимальный многочлен элемента x + algebraMap_A_B(a) над A равен композиции минимального многочлена x с преобразованием X ↦ X − C a, то есть minpoly_A(x + algebraMap_A_B(a)) = (minpoly_A x) ∘ (X − C a).

LaTeX

$$$\minpoly_A(x + \mathrm{algebraMap}_A^B(a)) = (\minpoly_A x) \circ (X - C a)$$$

Lean4

theorem add_algebraMap {B : Type*} [CommRing B] [Algebra A B] (x : B) (a : A) :
    minpoly A (x + algebraMap A B a) = (minpoly A x).comp (X - C a) :=
  by
  by_cases hx : IsIntegral A x
  · refine (minpoly.unique _ _ ((minpoly.monic hx).comp_X_sub_C _) ?_ fun 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_natDegree qmo.ne_zero, degree_eq_natDegree ((minpoly.monic hx).comp_X_sub_C _).ne_zero,
        natDegree_comp, natDegree_X_sub_C, mul_one]
      rwa [degree_eq_natDegree (minpoly.ne_zero hx), degree_eq_natDegree (qmo.comp_X_add_C _).ne_zero, natDegree_comp,
        natDegree_X_add_C, mul_one] at H
  · rw [minpoly.eq_zero hx, minpoly.eq_zero, zero_comp]
    refine fun h ↦ hx ?_
    simpa only [add_sub_cancel_right] using IsIntegral.sub h (isIntegral_algebraMap (x := a))

Похожие утверждения