mathlib3 documentation

set_theory.cardinal.divisibility

Cardinal Divisibility #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

source
@[simp]
theorem cardinal.is_unit_iff {a : cardinal} :
is_unit a ↔ a = 1
source
@[protected, instance]
def cardinal.units.unique  :
unique cardinalˣ
Equations
source
theorem cardinal.le_of_dvd {a b : cardinal} :
b ≠ 0 → a ∣ b → a ≤ b
source
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
source
@[simp]
theorem cardinal.prime_of_aleph_0_le {a : cardinal} (ha : cardinal.aleph_0 ≤ a) :
prime a
source
theorem cardinal.not_irreducible_of_aleph_0_le {a : cardinal} (ha : cardinal.aleph_0 ≤ a) :
¬irreducible a
source
@[simp, norm_cast]
theorem cardinal.nat_coe_dvd_iff {n m : ℕ} :
↑n ∣ ↑m ↔ n ∣ m
source
@[simp]
theorem cardinal.nat_is_prime_iff {n : ℕ} :
prime ↑n ↔ nat.prime n
source
theorem cardinal.is_prime_iff {a : cardinal} :
prime a ↔ cardinal.aleph_0 ≤ a ∨ ∃ (p : ℕ), a = ↑p ∧ nat.prime p
source
theorem cardinal.is_prime_pow_iff {a : cardinal} :
is_prime_pow a ↔ cardinal.aleph_0 ≤ a ∨ ∃ (n : ℕ), a = ↑n ∧ is_prime_pow n