order_finite_iff_ne_zero

Mathlib.RingTheory.PowerSeries.Order

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

English

order φ < ⊤ iff φ ≠ 0.

Русский

order φ < ⊤ тогда и только тогда φ ≠ 0.

LaTeX

$$(order(φ) < ⊤) ⇔ φ ≠ 0$$

Lean4

theorem order_finite_iff_ne_zero : (order φ < ⊤) ↔ φ ≠ 0 :=
  by
  simp only [order]
  split_ifs with h <;> simpa

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

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

Разделы

Аффилиация

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