English
For any x in a ring B that is an algebra over A, the minimal polynomial of −x over A is equal to (−1)^{natDegree(minpoly_A x)} times the composition of minpoly_A x with the polynomial −X; i.e., minpoly_A(−x) = (−1)^{natDegree(minpoly_A x)} · (minpoly_A x).comp(−X).
Русский
Для любого x из кольца B, являющегося алгеброй над A, минимальный полином −x над A равен (−1)^{natDegree(minpoly_A x)} умножить на (minpoly_A x) ∘ (−X).
LaTeX
$$$\minpoly_A(-x) = (-1)^{\operatorname{natDegree}(\minpoly_A x)} \cdot (\minpoly_A x) \circ (-X)$$$
Lean4
theorem neg {B : Type*} [Ring B] [Algebra A B] (x : B) :
minpoly A (-x) = (-1) ^ (natDegree (minpoly A x)) * (minpoly A x).comp (-X) :=
by
by_cases hx : IsIntegral A x
· refine (minpoly.unique _ _ ((minpoly.monic hx).neg_one_pow_natDegree_mul_comp_neg_X) ?_ fun q qmo hq => ?_).symm
· simp [aeval_comp]
· have : (Polynomial.aeval x) ((-1) ^ q.natDegree * q.comp (-X)) = 0 := by simpa [aeval_comp] using hq
have H := minpoly.min A x qmo.neg_one_pow_natDegree_mul_comp_neg_X this
have n1 := ((minpoly.monic hx).neg_one_pow_natDegree_mul_comp_neg_X).ne_zero
have n2 := qmo.neg_one_pow_natDegree_mul_comp_neg_X.ne_zero
rw [degree_eq_natDegree qmo.ne_zero, degree_eq_natDegree n1, natDegree_mul (by simp) (right_ne_zero_of_mul n1),
natDegree_comp]
rw [degree_eq_natDegree (minpoly.ne_zero hx),
degree_eq_natDegree qmo.neg_one_pow_natDegree_mul_comp_neg_X.ne_zero,
natDegree_mul (by simp) (right_ne_zero_of_mul n2), natDegree_comp] at H
simpa using H
· rw [minpoly.eq_zero hx, minpoly.eq_zero, zero_comp]
· simp only [natDegree_zero, pow_zero, mul_zero]
· exact IsIntegral.neg_iff.not.mpr hx
