of_constantCoeff_zero' — Mathlib

English

A variant version: if the constantCoeff of a power series a is 0 then HasSubst a.

Русский

Вариант: если константный коэффициент a равен нулю, то HasSubst a.

LaTeX

$$$\mathrm{constantCoeff}(a) = 0 \Rightarrow \mathrm{HasSubst}(a)$$$

Lean4

/-- A variant of `HasSubst.of_constantCoeff_zero` for `PowerSeries`
to avoid the expansion of `Unit`. -/
theorem of_constantCoeff_zero' {a : PowerSeries S} (ha : PowerSeries.constantCoeff a = 0) : HasSubst a :=
  HasSubst.of_constantCoeff_zero ha

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