normUnit_X

Mathlib.RingTheory.PowerSeries.Inverse

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

English

The normalization unit of X is 1: normUnit(X) = 1.

Русский

Нормализационная единица X равна 1: normUnit(X) = 1.

LaTeX

$$normUnit(X) = 1$$

Lean4

theorem normUnit_X : normUnit (X : k⟦X⟧) = 1 := by
  simp [normUnit, ← Units.val_eq_one, Unit_of_divided_by_X_pow_order_nonzero]

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

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

Разделы

Аффилиация

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