order_eq_top

Mathlib.RingTheory.PowerSeries.Order

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

← MathLib Explorer

English

φ.order = ⊤ iff φ = 0.

Русский

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

LaTeX

$$order(φ) = ⊤ ⇔ φ = 0$$

Lean4

/-- The `0` power series is the unique power series with infinite order. -/
@[simp]
theorem order_eq_top {φ : R⟦X⟧} : φ.order = ⊤ ↔ φ = 0 := by simpa using order_finite_iff_ne_zero.not_left

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

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

Разделы

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

Аффилиация

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