supDegree_zero — Mathlib

English

Let D : A → B be a map between a type A and a semilattice with bottom B. Then the supremum degree of the zero polynomial in the AddMonoidAlgebra R[A] with respect to D is the bottom element of B.

Русский

Пусть D : A → B; B имеет структуру нулевого элемента и полку верхних границ. ТогдаsupDegree D от нулевого многочлена в алгебре AddMonoidAlgebra R[A] равна нижней границе ⊥.

LaTeX

$$$(0 : R[A]).supDegree D = \bot$$$

Lean4

@[simp]
theorem supDegree_zero : (0 : R[A]).supDegree D = ⊥ := by simp [supDegree]

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