cardinalMk_eq

Mathlib.Algebra.MvPolynomial.Cardinal

URI: https://scilib.ai/kg/mathlib#MvPolynomial.cardinalMk_eq

English

For IsEmpty σ, the cardinality of MvPolynomial σ R equals the cardinality of R.

Русский

При пустом σ кардинал MvPolynomial σ R равен кардиналу R.

LaTeX

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

Lean4

theorem cardinalMk_eq [IsEmpty σ] : #(MvPolynomial σ R) = #R := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru