isUnit_divided_by_X_pow_order

Mathlib.RingTheory.PowerSeries.Inverse

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

← MathLib Explorer

English

If f ≠ 0, then divXPowOrder f is a unit in the power series ring.

Русский

Если f ≠ 0, то divXPowOrder f является единицей в кольце степенных рядов.

LaTeX

$$$ IsUnit(divXPowOrder(f)). $$$

Lean4

theorem isUnit_divided_by_X_pow_order {f : k⟦X⟧} (hf : f ≠ 0) : IsUnit (divXPowOrder f) :=
  ⟨Unit_of_divided_by_X_pow_order f, by simp only [Unit_of_divided_by_X_pow_order, dif_neg hf, Units.val_mk]⟩

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

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

Разделы

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

Аффилиация

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