cardinalMk_eq_one — Mathlib

English

If the coefficient ring R is a subsingleton, then the polynomial ring MvPolynomial σ R has cardinality 1.

Русский

Если кольцо коэффициентов R является подмножеством одного элемента, то размерность MvPolynomial σ R равна 1.

LaTeX

$$$\\#(\\mathrm{MvPolynomial}(\\sigma, R)) = 1$$$

Lean4

@[nontriviality]
theorem cardinalMk_eq_one [Subsingleton R] : #(MvPolynomial σ R) = 1 :=
  mk_eq_one _

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