cardinalMk_eq_lift — Mathlib

English

If σ is empty, the cardinality of MvPolynomial σ R equals the lifted cardinality of R: #(MvPolynomial σ R) = Cardinal.lift #R.

Русский

Если σ пусто, кардинал MvPolynomial σ R равен подъему кардинала #R: #(MvPolynomial σ R) = Cardinal.lift #R.

LaTeX

$$$\\#(\\mathrm{MvPolynomial}(\\sigma, R)) = \\operatorname{Cardinal.lift} (#R)$$$

Lean4

@[simp]
theorem cardinalMk_eq_lift [IsEmpty σ] : #(MvPolynomial σ R) = Cardinal.lift.{u} #R :=
  ((isEmptyRingEquiv R σ).toEquiv.trans Equiv.ulift.{u}.symm).cardinal_eq

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