degree_eq_bot_iff — Mathlib

English

For Laurent polynomial f, f.degree = ⊥ if and only if f = 0.

Русский

Для лаурентового многочлена f степень равна ⊥ тогда и только тогда, когда f = 0.

LaTeX

$$$\forall f : R[T;T^{-1}],\ f.degree = \bot \iff f = 0$$$

Lean4

@[simp]
theorem degree_eq_bot_iff {f : R[T;T⁻¹]} : f.degree = ⊥ ↔ f = 0 :=
  by
  refine ⟨fun h => ?_, fun h => by rw [h, degree_zero]⟩
  ext n
  simp only [coe_zero, Pi.zero_apply]
  simp_rw [degree, Finset.max_eq_sup_withBot, Finset.sup_eq_bot_iff, Finsupp.mem_support_iff, Ne, WithBot.coe_ne_bot,
    imp_false, not_not] at h
  exact h n

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