hasSubst_iff — Mathlib

English

For mv power series a, HasSubst a is equivalent to HasSubst (const Unit a).

Русский

Для многопеременного степенного ряда a, HasSubst a эквивалентно HasSubst (константный элемент Unit a).

LaTeX

$$$\mathrm{HasSubst}(a) \iff \mathrm{MvPowerSeries.HasSubst}(\mathrm{Function.const}\,\mathrm{Unit}\,a)$$$

Lean4

theorem hasSubst_iff {a : MvPowerSeries τ S} : HasSubst a ↔ MvPowerSeries.HasSubst (Function.const Unit a) :=
  ⟨fun ha ↦ MvPowerSeries.hasSubst_of_constantCoeff_nilpotent (Function.const Unit ha), fun ha ↦ (ha.const_coeff ())⟩

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