English
A symmetric variant asserting the same non-vanishing of constant term under injectivity in a symmetric setup.
Русский
Симметричная вариация утверждает то же неравенство константного коэффициента при инъективности в симметричной конфигурации.
LaTeX
$$(same structural content as 127316 with symmetry)$$
Lean4
theorem minpoly_coeff_zero_of_injective [Nontrivial R] (hf : Function.Injective f) : (minpoly R f).coeff 0 ≠ 0 :=
by
intro h
obtain ⟨P, hP⟩ := X_dvd_iff.2 h
have hdegP : P.degree < (minpoly R f).degree := by
rw [hP, mul_comm]
refine degree_lt_degree_mul_X fun h => ?_
rw [h, mul_zero] at hP
exact minpoly.ne_zero (isIntegral f) hP
have hPmonic : P.Monic :=
by
suffices (minpoly R f).Monic by rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this
exact minpoly.monic (isIntegral f)
have hzero : aeval f (minpoly R f) = 0 := minpoly.aeval _ _
simp only [hP, Module.End.mul_eq_comp, LinearMap.ext_iff, hf, aeval_X, map_eq_zero_iff, coe_comp, map_mul, zero_apply,
Function.comp_apply] at hzero
exact not_le.2 hdegP (minpoly.min _ _ hPmonic (LinearMap.ext hzero))
