isUnit_iff — Mathlib

English

Units of the mv polynomial ring are exactly constant units plus nilpotent higher terms vanish in unit criteria.

Русский

Единицы кольца mv-многочленов состоят ровно из константных единиц вместе с нильпотентными остальными коэффициентами; фактически, если константный коэффициент — единица, то прочие коэффициенты должны быть нильпотентны.

LaTeX

$$$$ \\IsUnit(P) \\iff \\operatorname{IsUnit}(P_0) \\wedge \\forall i \\\\neq 0, \\operatorname{IsNilpotent}(P_i). $$$$

Lean4

theorem isUnit_iff : IsUnit P ↔ IsUnit (P.coeff 0) ∧ ∀ i ≠ 0, IsNilpotent (P.coeff i) := by
  classical
  refine ⟨fun H ↦ ⟨H.map constantCoeff, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩
  · intro n hn
    obtain ⟨i, hi⟩ : ∃ i, n i ≠ 0 := by simpa [Finsupp.ext_iff] using hn
    let e := (optionEquivLeft _ _).symm.trans (renameEquiv R (Equiv.optionSubtypeNe i))
    have H := (Polynomial.coeff_isUnit_isNilpotent_of_isUnit (H.map e.symm)).2 (n i) hi
    simp only [ne_eq, isNilpotent_iff] at H
    convert ← H (n.equivMapDomain (Equiv.optionSubtypeNe i).symm).some
    refine (optionEquivLeft_coeff_coeff _ _ _ _).trans ?_
    simp [Finsupp.equivMapDomain_eq_mapDomain, coeff_rename_mapDomain _ (Equiv.optionSubtypeNe i).symm.injective]
  · have : IsNilpotent (P - C (P.coeff 0)) := by simp +contextual [isNilpotent_iff, apply_ite, eq_comm, h₂]
    simpa using this.isUnit_add_right_of_commute (h₁.map C) (.all _ _)

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