Commit 2023-02-24 10:36 6cd6039b

View on Github →

feat: Port SetTheory.Cardinal.Divisibility (#2473)

Estimated changes

Modified Mathlib.lean

Created Mathlib/SetTheory/Cardinal/Divisibility.lean

added theorem Cardinal.dvd_of_le_of_aleph0_le

added theorem Cardinal.isPrimePow_iff

added theorem Cardinal.isUnit_iff

added theorem Cardinal.is_prime_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_aleph0_le

added theorem Cardinal.prime_of_aleph0_le