hasSubst_of_constantCoeff_nilpotent

English

If σ is finite and each constantCoeff of a s is nilpotent, then HasSubst a.

Русский

Если σ конечна и для каждого s константный коэффициент a(s) нильпотентен, то HasSubst a.

LaTeX

$$HasSubst a$$

Lean4

/-- If `σ` is finite, then the nilpotent condition is enough for `HasSubst` -/
theorem hasSubst_of_constantCoeff_nilpotent [Finite σ] {a : σ → MvPowerSeries τ S}
    (ha : ∀ s, IsNilpotent (constantCoeff (a s))) : HasSubst a
    where
  const_coeff := ha
  coeff_zero _ := Set.toFinite _

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