Commit 2022-04-13 04:14 917fc964

View on Github →

refactor(set_theory/cofinality): Normalize names (#13400) We rename lemmas of the form is_regular (foo x) to is_regular_foo instead of foo_is_regular.

Estimated changes

Modified src/set_theory/cofinality.lean

deleted theorem cardinal.aleph'_succ_is_regular

deleted theorem cardinal.aleph_succ_is_regular

deleted theorem cardinal.cof_is_regular

added theorem cardinal.is_regular_aleph'_succ

added theorem cardinal.is_regular_aleph_succ

added theorem cardinal.is_regular_cof

added theorem cardinal.is_regular_omega

added theorem cardinal.is_regular_succ

deleted theorem cardinal.omega_is_regular

deleted theorem cardinal.succ_is_regular