Commit 2026-05-29 07:06 d526d13b

View on Github →

feat: values of preAleph.symm (#39713) For a cardinal c, preAleph.symm c returns the ordinal index of c, within the well-order of cardinals.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

deleted theorem Cardinal.preAleph_nat

added theorem Cardinal.preAleph_natCast

added theorem Cardinal.preAleph_ofNat

added theorem Cardinal.preAleph_symm_aleph0

added theorem Cardinal.preAleph_symm_aleph

added theorem Cardinal.preAleph_symm_natCast

added theorem Cardinal.preAleph_symm_ofNat

Modified Mathlib/SetTheory/Cardinal/Regular.lean

added theorem Cardinal.IsInaccessible.preAleph_symm_eq_ord

added theorem Cardinal.preAleph_symm_univ