zero

Mathlib.RingTheory.PowerSeries.Restricted

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

English

The zero power series is restricted for every parameter c.

Русский

Нулевой степенной ряд ограничен для любого параметра c.

LaTeX

$$$\mathrm{IsRestricted}(c, 0)$$$

Lean4

theorem zero : IsRestricted c (0 : PowerSeries R) := by simp [IsRestricted]

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

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

Разделы

Аффилиация

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