cardinalMk_le_max — Mathlib

English

The cardinality of the polynomial ring is bounded above by max(|R|, aleph0) for any ring R.

Русский

Кардинал множества R[X] не превосходит max(|R|, aleph0) для любого кольца R.

LaTeX

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

Lean4

theorem cardinalMk_le_max {R : Type u} [Semiring R] : #(R[X]) ≤ max #R ℵ₀ :=
  by
  cases subsingleton_or_nontrivial R
  · exact (mk_eq_one _).trans_le (le_max_of_le_right one_le_aleph0)
  · exact cardinalMk_eq_max.le

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