supDegree_single_ne_zero — Mathlib

English

If the scalar r is nonzero, the supremum degree of the single element δ_a r equals D(a). If r=0, it's the bottom element.

Русский

Если скаляр r не равен нулю, верхняя грань степени единичного элемента δ_a r равна D(a); иначе равна ⊥.

LaTeX

$$$\\supDegree D (\\,\\text{single } a r\\,) = \\begin{cases} ⊥, & r=0 \\\\ D(a), & r\\neq 0 \\end{cases}$$$

Lean4

theorem supDegree_single_ne_zero (a : A) {r : R} (hr : r ≠ 0) : (single a r).supDegree D = D a := by
  rw [supDegree, Finsupp.support_single_ne_zero a hr, Finset.sup_singleton]

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