Commit 2024-02-12 23:48 a6f14574

View on Github →

fix(Cardinal): fix theorem names (#10465) Remove unnecessary of_lt_aleph_0 from 2 theorem names. Also fix typos in the comments of 2 other files.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

added theorem Cardinal.add_nat_le_add_nat_iff

deleted theorem Cardinal.add_nat_le_add_nat_iff_of_lt_aleph_0

added theorem Cardinal.add_one_le_add_one_iff

deleted theorem Cardinal.add_one_le_add_one_iff_of_lt_aleph_0

Modified Mathlib/SetTheory/Ordinal/Basic.lean