order_eq_zero_iff' — Mathlib

English

The order is zero if and only if p = 0 or p 0 ≠ 0, equivalently p.order = 0 ↔ p = 0 ∨ p(0) ≠ 0.

Русский

Порядок равен нулю тогда и только тогда, когда p = 0 или p(0) ≠ 0.

LaTeX

$$$p.\\mathrm{order}=0 \\;\\Leftrightarrow\\; p=0 \\lor p(0) \\neq 0$$$

Lean4

theorem order_eq_zero_iff' : p.order = 0 ↔ p = 0 ∨ p 0 ≠ 0 := by
  simpa [order, Nat.sInf_eq_zero, FormalMultilinearSeries.ext_iff, eq_empty_iff_forall_notMem] using or_comm

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