feat(set_theory/cardinal_divisibility): add lemmas about divisibility in the cardinals (#12197)

Author: ericrbg

src/set_theory/cardinal.lean

@@ -907,6 +907,10 @@ begin
   rintro (rfl|rfl|⟨ha,hb⟩); simp only [*, mul_lt_omega, omega_pos, zero_mul, mul_zero]
 end
 
+lemma omega_le_mul_iff {a b : cardinal} : ω ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ω ≤ a ∨ ω ≤ b) :=
+let h := (@mul_lt_omega_iff a b).not in
+by rwa [not_lt, not_or_distrib, not_or_distrib, not_and_distrib, not_lt, not_lt] at h
+
 lemma mul_lt_omega_iff_of_ne_zero {a b : cardinal} (ha : a ≠ 0) (hb : b ≠ 0) :
   a * b < ω ↔ a < ω ∧ b < ω :=
 by simp [mul_lt_omega_iff, ha, hb]

src/set_theory/cardinal_divisibility.lean

@@ -0,0 +1,141 @@
+/-
+Copyright (c) 2022 Eric Rodriguez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Rodriguez
+-/
+
+import set_theory.cardinal_ordinal
+import algebra.is_prime_pow
+
+/-!
+# 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_omega_le`), showing that the
+cardinal numbers do not form a `comm_cancel_monoid_with_zero`.
+
+## Main results
+
+* `cardinal.prime_of_omega_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.is_prime_pow_iff`: a `cardinal` is a prime power iff it is infinite or a natural number
+  which is itself a prime power.
+
+-/
+
+namespace cardinal
+
+open_locale cardinal
+
+universe u
+variables {a b : cardinal.{u}} {n m : ℕ}
+
+@[simp] lemma is_unit_iff : is_unit a ↔ a = 1 :=
+begin
+  refine ⟨λ h, _, by { rintro rfl, exact is_unit_one }⟩,
+  rcases eq_or_ne a 0 with rfl | ha,
+  { exact (not_is_unit_zero h).elim },
+  rw is_unit_iff_forall_dvd at h,
+  cases h 1 with t ht,
+  rw [eq_comm, mul_eq_one_iff'] at ht,
+  { exact ht.1 },
+  all_goals { rwa one_le_iff_ne_zero },
+  { rintro rfl,
+    rw mul_zero at ht,
+    exact zero_ne_one ht }
+end
+
+theorem le_of_dvd : ∀ {a b : cardinal}, b ≠ 0 → a ∣ b → a ≤ b
+| a _ b0 ⟨b, rfl⟩ := by simpa only [mul_one] using mul_le_mul_left'
+  (one_le_iff_ne_zero.2 (λ h : b = 0, by simpa only [h, mul_zero] using b0)) a
+
+lemma dvd_of_le_of_omega_le (ha : a ≠ 0) (h : a ≤ b) (hb : ω ≤ b) : a ∣ b :=
+⟨b, (mul_eq_right hb h ha).symm⟩
+
+@[simp] lemma prime_of_omega_le (ha : ω ≤ a) : prime a :=
+begin
+  refine ⟨(omega_pos.trans_le ha).ne', _, λ b c hbc, _⟩,
+  { rw is_unit_iff,
+    exact (one_lt_omega.trans_le ha).ne' },
+  cases eq_or_ne (b * c) 0 with hz hz,
+  { rcases mul_eq_zero.mp hz with rfl | rfl; simp },
+  wlog h : c ≤ b,
+  left,
+  have habc := le_of_dvd hz hbc,
+  rwa [mul_eq_max' $ ha.trans $ habc, max_def, if_pos h] at hbc
+end
+
+lemma not_irreducible_of_omega_le (ha : ω ≤ a) : ¬irreducible a :=
+begin
+  rw [irreducible_iff, not_and_distrib],
+  refine or.inr (λ h, _),
+  simpa [mul_omega_eq ha, is_unit_iff, (one_lt_omega.trans_le ha).ne', one_lt_omega.ne'] using h a ω
+end
+
+@[simp, norm_cast] lemma nat_coe_dvd_iff : (n : cardinal) ∣ m ↔ n ∣ m :=
+begin
+  refine ⟨_, λ ⟨h, ht⟩, ⟨h, by exact_mod_cast ht⟩⟩,
+  rintro ⟨k, hk⟩,
+  have : ↑m < ω := nat_lt_omega m,
+  rw [hk, mul_lt_omega_iff] at this,
+  rcases this with h | h | ⟨-, hk'⟩,
+  iterate 2 { simp only [h, mul_zero,  zero_mul, nat.cast_eq_zero] at hk, simp [hk] },
+  lift k to ℕ using hk',
+  exact ⟨k, by exact_mod_cast hk⟩
+end
+
+@[simp] lemma nat_is_prime_iff : prime (n : cardinal) ↔ n.prime :=
+begin
+  simp only [prime, nat.prime_iff],
+  refine and_congr (by simp) (and_congr _ ⟨λ h b c hbc, _, λ h b c hbc, _⟩),
+  { simp only [is_unit_iff, nat.is_unit_iff],
+    exact_mod_cast iff.rfl },
+  { exact_mod_cast h b c (by exact_mod_cast hbc) },
+  cases lt_or_le (b * c) ω with h' h',
+  { rcases mul_lt_omega_iff.mp h' with rfl | rfl | ⟨hb, hc⟩,
+    { simp },
+    { simp },
+    lift b to ℕ using hb,
+    lift c to ℕ using hc,
+    exact_mod_cast h b c (by exact_mod_cast hbc) },
+  rcases omega_le_mul_iff.mp h' with ⟨hb, hc, hω⟩,
+  have hn : (n : cardinal) ≠ 0,
+  { intro h,
+    rw [h, zero_dvd_iff, mul_eq_zero] at hbc,
+    cases hbc; contradiction },
+  wlog hω : ω ≤ b := hω using [b c],
+  exact or.inl (dvd_of_le_of_omega_le hn ((nat_lt_omega n).le.trans hω) hω),
+end
+
+lemma is_prime_iff {a : cardinal} : prime a ↔ ω ≤ a ∨ ∃ p : ℕ, a = p ∧ p.prime :=
+begin
+  cases le_or_lt ω a with h h,
+  { simp [h] },
+  lift a to ℕ using id h,
+  simp [not_le.mpr h]
+end
+
+lemma is_prime_pow_iff {a : cardinal} : is_prime_pow a ↔ ω ≤ a ∨ ∃ n : ℕ, a = n ∧ is_prime_pow n :=
+begin
+  by_cases h : ω ≤ a,
+  { simp [h, (prime_of_omega_le h).is_prime_pow] },
+  lift a to ℕ using not_le.mp h,
+  simp only [h, nat.cast_inj, exists_eq_left', false_or, is_prime_pow_nat_iff],
+  rw is_prime_pow_def,
+  split,
+  swap,
+  { rintro ⟨p, k, hp, hk, rfl⟩,
+    exact ⟨p, k, nat_is_prime_iff.mpr hp, by exact_mod_cast hk, by norm_cast⟩ },
+  rintro ⟨p, k, hp, hk, hpk⟩,
+  have key : _ ≤ p ^ k :=
+    power_le_power_left hp.ne_zero (show (1 : cardinal) ≤ k, by exact_mod_cast hk),
+  rw [power_one, hpk] at key,
+  lift p to ℕ using key.trans_lt (nat_lt_omega a),
+  exact ⟨p, k, nat_is_prime_iff.mp hp, hk, by exact_mod_cast hpk⟩
+end
+
+end cardinal

src/set_theory/cardinal_ordinal.lean

@@ -371,6 +371,13 @@ begin
   convert mul_le_mul_left' (one_le_iff_ne_zero.mpr h') _, rw [mul_one],
 end
 
+lemma mul_eq_max' {a b : cardinal} (h : ω ≤ a * b) : a * b = max a b :=
+begin
+  rcases omega_le_mul_iff.mp h with ⟨ha, hb, h⟩,
+  wlog h : ω ≤ a := h using [a b],
+  exact mul_eq_max_of_omega_le_left h hb
+end
+
 theorem mul_le_max (a b : cardinal) : a * b ≤ max (max a b) ω :=
 begin
   by_cases ha0 : a = 0,