of_constantCoeff_zero

Mathlib.RingTheory.PowerSeries.Substitution

URI: https://scilib.ai/kg/mathlib#PowerSeries.HasSubst.of_constantCoeff_zero

English

If the constantCoeff of a mv power series a is 0, then HasSubst a.

Русский

Если константный коэффициент mv PowerSeries a равен 0, то HasSubst a.

LaTeX

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

Lean4

theorem of_constantCoeff_zero {a : MvPowerSeries τ S} (ha : MvPowerSeries.constantCoeff a = 0) : HasSubst a := by
  simp [HasSubst, ha]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru