degreesLE_zero — Mathlib

English

The degrees bound at zero equals the whole unit submodule.

Русский

Граница степеней при нуле равна единице как подмодуль.

LaTeX

$$$\\\\operatorname{degreesLE}(R,\\\\sigma, 0) = 1$$$

Lean4

@[simp]
theorem degreesLE_zero : degreesLE R σ 0 = 1 :=
  by
  refine le_antisymm (fun x hx ↦ ?_) (by simp)
  simp only [mem_degreesLE, nonpos_iff_eq_zero] at hx
  have :=
    (totalDegree_eq_zero_iff_eq_C (p := x)).mp
      (Nat.eq_zero_of_le_zero (x.totalDegree_le_degrees_card.trans (by simp [hx])))
  exact ⟨x.coeff 0, by simp [Algebra.smul_def, ← this]⟩

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