Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-03 21:31 f549c103

View on Github →

feat(set_theory/cardinal_divisibility): add lemmas about divisibility in the cardinals (#12197)

Estimated changes

Modified src/set_theory/cardinal.lean

added theorem cardinal.omega_le_mul_iff

Created src/set_theory/cardinal_divisibility.lean

added theorem cardinal.dvd_of_le_of_omega_le

added theorem cardinal.is_prime_iff

added theorem cardinal.is_prime_pow_iff

added theorem cardinal.is_unit_iff

added theorem cardinal.le_of_dvd

added theorem cardinal.nat_coe_dvd_iff

added theorem cardinal.nat_is_prime_iff

added theorem cardinal.not_irreducible_of_omega_le

added theorem cardinal.prime_of_omega_le

Modified src/set_theory/cardinal_ordinal.lean

added theorem cardinal.mul_eq_max'