invOneSubPow_zero

Mathlib.RingTheory.PowerSeries.WellKnown

URI: https://scilib.ai/kg/mathlib#PowerSeries.invOneSubPow_zero

English

The inverse of the zeroth subpower is the constant 1: invOneSubPow S 0 = 1.

Русский

Обратная нулевой подстепени равна единице: invOneSubPow S 0 = 1.

LaTeX

$$$$ invOneSubPow\, S\, 0 = 1 $$$$

Lean4

theorem invOneSubPow_zero : invOneSubPow S 0 = 1 :=
  by
  delta invOneSubPow
  simp only

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

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

Разделы

Аффилиация

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