cardinalMk_eq_max — Mathlib

English

For any semiring R with at least two elements, the cardinality of the polynomial ring R[X] equals the maximum of the cardinality of R and aleph-null.

Русский

Для не тривиального кольца R множество полиномов R[X] имеет кардинал равный max(|R|, aleph_0).

LaTeX

$$$\\#(R[X]) = \\max(\\#R, \\aleph_0).$$$

Lean4

@[simp]
theorem cardinalMk_eq_max {R : Type u} [Semiring R] [Nontrivial R] : #(R[X]) = max #R ℵ₀ :=
  (toFinsuppIso R).toEquiv.cardinal_eq.trans <|
    by
    rw [AddMonoidAlgebra, mk_finsupp_lift_of_infinite, lift_uzero, max_comm]
    rfl

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