Unit_of_divided_by_X_pow_order_zero

Mathlib.RingTheory.PowerSeries.Inverse

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

← MathLib Explorer

English

For f = 0, the unit of divXPowOrder is 1.

Русский

Для f = 0 единица divXPowOrder равна 1.

LaTeX

$$$ Unit\_of\_divided\_by\_X\_pow\_order(0) = 1. $$$

Lean4

@[simp]
theorem Unit_of_divided_by_X_pow_order_zero : Unit_of_divided_by_X_pow_order (0 : k⟦X⟧) = 1 := by
  simp only [Unit_of_divided_by_X_pow_order, dif_pos]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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