Documentation

Mathlib.SetTheory.Cardinal.Divisibility

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_aleph0_le), showing that the cardinal numbers do not form a CancelCommMonoidWithZero.

Main results #

@[simp]
theorem Cardinal.le_of_dvd {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} :
b 0a ba b
theorem Cardinal.dvd_of_le_of_aleph0_le {a : Cardinal.{u}} {b : Cardinal.{u}} (ha : a 0) (h : a b) (hb : Cardinal.aleph0 b) :
a b
@[simp]
theorem Cardinal.nat_coe_dvd_iff {n : } {m : } :
n m n m
@[simp]
theorem Cardinal.nat_is_prime_iff {n : } :
Prime n n.Prime
theorem Cardinal.is_prime_iff {a : Cardinal.{u_1}} :
Prime a Cardinal.aleph0 a ∃ (p : ), a = p p.Prime