IsNilpotent_subst — Mathlib

English

If a substitution a is given and the constant term of f is nilpotent, then the constant term of the substituted f is also nilpotent.

Русский

Если дана подстановка a и константный коэффициент f явлется нильпотентным, то константный коэффициент подстановки f также нильпотентен.

LaTeX

$$$\text{If } hf : \operatorname{IsNilpotent}(\mathrm{constantCoeff}(f)) \text{ then } \operatorname{IsNilpotent}(\mathrm{constantCoeff}(\operatorname{substAlgHom}(ha)\, f)).$$$

Lean4

theorem IsNilpotent_subst (ha : HasSubst a) {f : MvPowerSeries σ R} (hf : IsNilpotent (constantCoeff f)) :
    IsNilpotent (constantCoeff (substAlgHom ha f)) := by
  classical
  rw [coe_substAlgHom, constantCoeff_subst ha]
  apply isNilpotent_finsum
  intro d
  by_cases hd : d = 0
  · rw [← algebraMap_smul S, smul_eq_mul, mul_comm, ← smul_eq_mul, hd]
    apply IsNilpotent.smul
    simpa using IsNilpotent.map hf (algebraMap R S)
  · apply IsNilpotent.smul
    rw [← ne_eq, Finsupp.ne_iff] at hd
    obtain ⟨t, hs⟩ := hd
    rw [← Finsupp.prod_filter_mul_prod_filter_not (fun i ↦ i = t), map_mul, mul_comm, ← smul_eq_mul]
    apply IsNilpotent.smul
    rw [Finsupp.prod_eq_single t]
    · simpa using IsNilpotent.pow_of_pos (ha.const_coeff t) hs
    · intro t' htt' ht'
      simp [ht'] at htt'
    · exact fun _ ↦ by rw [pow_zero]

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