degree_of_subsingleton — Mathlib

English

If the coefficient ring is a subsingleton, then the degree of any polynomial is the bottom element.

Русский

Если кольцо коэффициентов состоит из одного элемента, то степень любого многочлена равна нижней границе.

LaTeX

$$$[\\text{Subsingleton } R] \\Rightarrow \\operatorname{degree}(p) = \\bot$$$

Lean4

@[nontriviality]
theorem degree_of_subsingleton [Subsingleton R] : degree p = ⊥ := by rw [Subsingleton.elim p 0, degree_zero]

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