hasSubst_of_constantCoeff_zero — Mathlib

English

Let a be a family a : σ → MvPowerSeries τ S. If σ is finite and every a(s) has zero constant coefficient, then a substitution operation HasSubst a exists.

Русский

Пусть a : σ → MvPowerSeries τ S — семейство степенных рядов. Если σ конечно или в точности Finite(σ) и для каждого s выполняется constantCoeff(a(s)) = 0, то существует подстановка HasSubst a.

LaTeX

$$$ \\operatorname{Finite}(\\sigma) \\Rightarrow \\left( \\forall s, \\operatorname{constantCoeff}(a(s)) = 0 \\right) \\Rightarrow \\operatorname{HasSubst} a $$$

Lean4

/-- If `σ` is finite, then having zero constant coefficient is enough for `HasSubst` -/
theorem hasSubst_of_constantCoeff_zero [Finite σ] {a : σ → MvPowerSeries τ S} (ha : ∀ s, constantCoeff (a s) = 0) :
    HasSubst a :=
  hasSubst_of_constantCoeff_nilpotent (fun s ↦ by simp only [ha s, IsNilpotent.zero])

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