ne_zero_iff_order_finite

Mathlib.RingTheory.MvPowerSeries.Order

URI: https://scilib.ai/kg/mathlib#MvPowerSeries.ne_zero_iff_order_finite

English

f ≠ 0 iff f.order.toNat = f.order

Русский

f ≠ 0 тогда f.order.toNat = f.order

LaTeX

$$f ≠ 0 ↔ f.order.toNat = f.order$$

Lean4

theorem ne_zero_iff_order_finite : f ≠ 0 ↔ f.order.toNat = f.order :=
  ne_zero_iff_weightedOrder_finite 1

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

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

Разделы

Аффилиация

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