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 cancellative CommMonoidWithZero.

Main results

• Cardinal.prime_of_aleph0_le: a Cardinal is prime if it is infinite.
• Cardinal.is_prime_iff: a Cardinal is prime iff it is infinite or a prime natural number.
• Cardinal.isPrimePow_iff: a Cardinal is a prime power iff it is infinite or a natural number which is itself a prime power.

@[instance_reducible]

instance Cardinal.instUniqueUnits : Unique Cardinal.{u}ˣ

Equations

• Cardinal.instUniqueUnits = { default := 1, uniq := Cardinal.instUniqueUnits._proof_5 }

@[deprecated isUnit_iff_eq_one (since := "2026-09-20")]

theorem Cardinal.isUnit_iff {M : Type u_1} [Monoid M] {a : M} [Subsingleton Mˣ] : IsUnit a ↔ a = 1

Alias of isUnit_iff_eq_one.

@[simp]

theorem Cardinal.prime_of_aleph0_le {a : Cardinal.{u}} (ha : aleph0 ≤ a) : Prime a

theorem Cardinal.not_irreducible_of_aleph0_le {a : Cardinal.{u}} (ha : aleph0 ≤ a) : ¬Irreducible a

@[simp]

theorem Cardinal.prime_natCast_iff {n : ℕ} : Prime ↑n ↔ Nat.Prime n

@[deprecated Cardinal.prime_natCast_iff (since := "2026-09-20")]

theorem Cardinal.nat_is_prime_iff {n : ℕ} : Prime ↑n ↔ Nat.Prime n

Alias of Cardinal.prime_natCast_iff.

theorem Cardinal.prime_iff {a : Cardinal.{u_1}} : Prime a ↔ aleph0 ≤ a ∨ ∃ (p : ℕ), a = ↑p ∧ Nat.Prime p

@[deprecated Cardinal.prime_iff (since := "2026-09-20")]

theorem Cardinal.is_prime_iff {a : Cardinal.{u_1}} : Prime a ↔ aleph0 ≤ a ∨ ∃ (p : ℕ), a = ↑p ∧ Nat.Prime p

Alias of Cardinal.prime_iff.

theorem Cardinal.isPrimePow_iff {a : Cardinal.{u_1}} : IsPrimePow a ↔ aleph0 ≤ a ∨ ∃ (n : ℕ), a = ↑n ∧ IsPrimePow n