zero'

Mathlib.RingTheory.PowerSeries.Substitution

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

English

A variant stating HasSubst 0 holds, without further elaboration.

Русский

Вариант утверждения, что HasSubst 0 выполняется.

LaTeX

$$$\mathrm{zero'} : \HasSubst(0)$$$

Lean4

/-- A variant of `HasSubst.zero` to avoid the expansion of `Unit`. -/
theorem zero' : HasSubst (0 : PowerSeries R) :=
  PowerSeries.HasSubst.zero

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

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

Разделы

Аффилиация

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