Commit 2026-10-27 21:33 49cd7a79

View on Github →

chore(SetTheory/Cardinal/Divisibility): golf file (#44013) We also move a few theorems about divisibility to an earlier file, and perform some renames.

Estimated changes

added theorem Cardinal.le_of_dvd
added theorem Cardinal.aleph0_ne_one
modified theorem Cardinal.one_le_aleph0
modified theorem Cardinal.one_lt_aleph0
deleted theorem Cardinal.isUnit_iff
deleted theorem Cardinal.is_prime_iff
deleted theorem Cardinal.le_of_dvd
deleted theorem Cardinal.nat_is_prime_iff
added theorem Cardinal.prime_iff