Cardinal Divisibility #
We show basic results about divisibility in the cardinal numbers. This relation can be characterised
in the following simple way: if a
and b
are both less than ℵ₀
, then a ∣ b
iff they are
divisible as natural numbers. If b
is greater than ℵ₀
, then a ∣ b
iff a ≤ b
. This
furthermore shows that all infinite cardinals are prime; recall that a * b = max a b
if
ℵ₀ ≤ a * b
; therefore a ∣ b * c = a ∣ max b c
and therefore clearly either a ∣ b
or a ∣ c
.
Note furthermore that no infinite cardinal is irreducible
(cardinal.not_irreducible_of_aleph_0_le
), showing that the cardinal numbers do not form a
comm_cancel_monoid_with_zero
.
Main results #
cardinal.prime_of_aleph_0_le
: acardinal
is prime if it is infinite.cardinal.is_prime_iff
: acardinal
is prime iff it is infinite or a prime natural number.cardinal.is_prime_pow_iff
: acardinal
is a prime power iff it is infinite or a natural number which is itself a prime power.
@[protected, instance]
Equations
- cardinal.units.unique = {to_inhabited := {default := 1}, uniq := cardinal.units.unique._proof_1}
theorem
cardinal.dvd_of_le_of_aleph_0_le
{a b : cardinal}
(ha : a ≠ 0)
(h : a ≤ b)
(hb : cardinal.aleph_0 ≤ b) :
a ∣ b
@[simp]
theorem
cardinal.is_prime_pow_iff
{a : cardinal} :
is_prime_pow a ↔ cardinal.aleph_0 ≤ a ∨ ∃ (n : ℕ), a = ↑n ∧ is_prime_pow n