Commit 2022-03-14 07:05 7b7fea55

View on Github →

refactor(set_theory/cardinal_ordinal): aleph_is_principal_aleph → principal_add_aleph (#12663) This matches the naming scheme used throughout set_theory/principal.lean.

Estimated changes

Modified src/set_theory/cardinal_ordinal.lean

deleted theorem cardinal.aleph_is_principal_add

deleted theorem cardinal.ord_is_principal_add

added theorem cardinal.principal_add_aleph

added theorem cardinal.principal_add_ord