From 80586b926dc731afee5a50ab40f9808d1c850eea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Wed, 10 Aug 2022 16:27:15 -0500 Subject: [PATCH 1/6] more lemmas on mods --- src/set_theory/ordinal/arithmetic.lean | 25 ++++++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/src/set_theory/ordinal/arithmetic.lean b/src/set_theory/ordinal/arithmetic.lean index 412256ad8878a..689abb5e6892c 100644 --- a/src/set_theory/ordinal/arithmetic.lean +++ b/src/set_theory/ordinal/arithmetic.lean @@ -554,7 +554,7 @@ protected theorem sub_eq_zero_iff_le {a b : ordinal} : a - b = 0 ↔ a ≤ b := theorem sub_sub (a b c : ordinal) : a - b - c = a - (b + c) := eq_of_forall_ge_iff $ λ d, by rw [sub_le, sub_le, sub_le, add_assoc] -theorem add_sub_add_cancel (a b c : ordinal) : a + b - (a + c) = b - c := +@[simp] theorem add_sub_add_cancel (a b c : ordinal) : a + b - (a + c) = b - c := by rw [← sub_sub, add_sub_cancel] theorem sub_is_limit {a b} (l : is_limit a) (h : b < a) : is_limit (a - b) := @@ -879,6 +879,8 @@ instance : has_mod ordinal := ⟨λ a b, a - b * (a / b)⟩ theorem mod_def (a b : ordinal) : a % b = a - b * (a / b) := rfl +theorem mod_le (a b : ordinal) : a % b ≤ a := sub_le_self a _ + @[simp] theorem mod_zero (a : ordinal) : a % 0 = a := by simp only [mod_def, div_zero, zero_mul, sub_zero] @@ -916,6 +918,24 @@ end theorem dvd_iff_mod_eq_zero {a b : ordinal} : b ∣ a ↔ a % b = 0 := ⟨mod_eq_zero_of_dvd, dvd_of_mod_eq_zero⟩ +@[simp] theorem mul_add_mod_self (x y z : ordinal) : (x * y + z) % x = z % x := +begin + rcases eq_or_ne x 0 with rfl | hx, + { simp }, + { rwa [mod_def, mul_add_div, mul_add, ←sub_sub, add_sub_cancel, mod_def] } +end + +@[simp] theorem mul_mod (x y : ordinal) : x * y % x = 0 := by simpa using mul_add_mod_self x y 0 + +theorem mod_mod_of_dvd (a : ordinal) {b c : ordinal} (h : c ∣ b) : a % b % c = a % c := +begin + nth_rewrite_rhs 0 ←div_add_mod a b, + rcases h with ⟨d, rfl⟩, + rw [mul_assoc, mul_add_mod_self] +end + +@[simp] theorem mod_mod (a b : ordinal) : a % b % b = a % b := mod_mod_of_dvd a dvd_rfl + /-! ### Families of ordinals There are two kinds of indexed families that naturally arise when dealing with ordinals: those @@ -1988,6 +2008,9 @@ begin exact (opow_le_of_limit (opow_ne_zero _ a0) l).symm } end +theorem pow_dvd_pow (o : ordinal) {a b : ordinal} (h : a ≤ b) : o ^ a ∣ o ^ b := +⟨o ^ (b - a), by rw [←opow_add, ordinal.add_sub_cancel_of_le h]⟩ + /-! ### Ordinal logarithm -/ /-- The ordinal logarithm is the solution `u` to the equation `x = b ^ u * v + w` where `v < b` and From 49512914cdd09382108957a43847b1a0896d2eb1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Wed, 10 Aug 2022 16:36:43 -0500 Subject: [PATCH 2/6] golf --- src/set_theory/ordinal/arithmetic.lean | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/src/set_theory/ordinal/arithmetic.lean b/src/set_theory/ordinal/arithmetic.lean index 689abb5e6892c..9d9157144cb65 100644 --- a/src/set_theory/ordinal/arithmetic.lean +++ b/src/set_theory/ordinal/arithmetic.lean @@ -1977,12 +1977,10 @@ end theorem opow_one_add (a b : ordinal) : a ^ (1 + b) = a * a ^ b := by rw [opow_add, opow_one] -theorem opow_dvd_opow (a) {b c : ordinal} - (h : b ≤ c) : a ^ b ∣ a ^ c := -by { rw [← ordinal.add_sub_cancel_of_le h, opow_add], apply dvd_mul_right } +theorem opow_dvd_opow (a) {b c : ordinal} (h : b ≤ c) : a ^ b ∣ a ^ c := +⟨a ^ (c - b), by rw [←opow_add, ordinal.add_sub_cancel_of_le h] ⟩ -theorem opow_dvd_opow_iff {a b c : ordinal} - (a1 : 1 < a) : a ^ b ∣ a ^ c ↔ b ≤ c := +theorem opow_dvd_opow_iff {a b c : ordinal} (a1 : 1 < a) : a ^ b ∣ a ^ c ↔ b ≤ c := ⟨λ h, le_of_not_lt $ λ hn, not_le_of_lt ((opow_lt_opow_iff_right a1).2 hn) $ le_of_dvd (opow_ne_zero _ $ one_le_iff_ne_zero.1 $ a1.le) h, @@ -2008,9 +2006,6 @@ begin exact (opow_le_of_limit (opow_ne_zero _ a0) l).symm } end -theorem pow_dvd_pow (o : ordinal) {a b : ordinal} (h : a ≤ b) : o ^ a ∣ o ^ b := -⟨o ^ (b - a), by rw [←opow_add, ordinal.add_sub_cancel_of_le h]⟩ - /-! ### Ordinal logarithm -/ /-- The ordinal logarithm is the solution `u` to the equation `x = b ^ u * v + w` where `v < b` and From 0ef12a24c6b70e2d74b7911cf84cbba84605c0b4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Wed, 10 Aug 2022 18:31:57 -0500 Subject: [PATCH 3/6] fix --- src/set_theory/ordinal/notation.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/set_theory/ordinal/notation.lean b/src/set_theory/ordinal/notation.lean index 3694d168a3204..23d2f085f3de3 100644 --- a/src/set_theory/ordinal/notation.lean +++ b/src/set_theory/ordinal/notation.lean @@ -428,7 +428,7 @@ instance sub_NF (o₁ o₂) : ∀ [NF o₁] [NF o₂], NF (o₁ - o₂) { change e₁ = e₂ at ee, substI e₂, unfold sub._match_1, cases mn : (n₁:ℕ) - n₂; dsimp only [sub._match_2], { by_cases en : n₁ = n₂, - { simp [en], rwa [add_sub_add_cancel] }, + { simpa [en] }, { simp [en, -repr], exact (ordinal.sub_eq_zero_iff_le.2 $ le_of_lt $ oadd_lt_oadd_2 h₁ $ lt_of_le_of_ne (tsub_eq_zero_iff_le.1 mn) (mt pnat.eq en)).symm } }, From 58fa659a6554e2cac0d2089176524dcd6e6bd429 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Thu, 11 Aug 2022 10:21:32 -0500 Subject: [PATCH 4/6] add lemma --- src/set_theory/ordinal/arithmetic.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/set_theory/ordinal/arithmetic.lean b/src/set_theory/ordinal/arithmetic.lean index 9d9157144cb65..034a71ce854eb 100644 --- a/src/set_theory/ordinal/arithmetic.lean +++ b/src/set_theory/ordinal/arithmetic.lean @@ -2169,6 +2169,14 @@ begin rw [add_zero, mul_one] end +theorem div_opow_log_pos (b : ordinal) {o : ordinal} (ho : o ≠ 0) : 0 < o / b ^ log b o := +begin + rcases eq_zero_or_pos b with (rfl | hb), + { simpa using ordinal.pos_iff_ne_zero.2 ho }, + { rw div_pos (opow_ne_zero _ hb.ne'), + exact opow_log_le_self b ho } +end + theorem div_opow_log_lt {b : ordinal} (o : ordinal) (hb : 1 < b) : o / b ^ log b o < b := begin rw [div_lt (opow_pos _ (zero_lt_one.trans hb)).ne', ←opow_succ], From 7847e30e153c15bcd90cfa0b61ca3eaf9d0a94d5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Wed, 1 Mar 2023 03:28:07 -0600 Subject: [PATCH 5/6] merge --- src/set_theory/ordinal/exponential.lean | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/src/set_theory/ordinal/exponential.lean b/src/set_theory/ordinal/exponential.lean index 4b210acb5a2fe..4aa9749f45ebd 100644 --- a/src/set_theory/ordinal/exponential.lean +++ b/src/set_theory/ordinal/exponential.lean @@ -189,12 +189,10 @@ end theorem opow_one_add (a b : ordinal) : a ^ (1 + b) = a * a ^ b := by rw [opow_add, opow_one] -theorem opow_dvd_opow (a) {b c : ordinal} - (h : b ≤ c) : a ^ b ∣ a ^ c := -by { rw [← ordinal.add_sub_cancel_of_le h, opow_add], apply dvd_mul_right } +theorem opow_dvd_opow (a) {b c : ordinal} (h : b ≤ c) : a ^ b ∣ a ^ c := +⟨a ^ (c - b), by rw [←opow_add, ordinal.add_sub_cancel_of_le h] ⟩ -theorem opow_dvd_opow_iff {a b c : ordinal} - (a1 : 1 < a) : a ^ b ∣ a ^ c ↔ b ≤ c := +theorem opow_dvd_opow_iff {a b c : ordinal} (a1 : 1 < a) : a ^ b ∣ a ^ c ↔ b ≤ c := ⟨λ h, le_of_not_lt $ λ hn, not_le_of_lt ((opow_lt_opow_iff_right a1).2 hn) $ le_of_dvd (opow_ne_zero _ $ one_le_iff_ne_zero.1 $ a1.le) h, @@ -384,6 +382,14 @@ begin rw [add_zero, mul_one] end +theorem div_opow_log_pos (b : ordinal) {o : ordinal} (ho : o ≠ 0) : 0 < o / b ^ log b o := +begin + rcases eq_zero_or_pos b with (rfl | hb), + { simpa using ordinal.pos_iff_ne_zero.2 ho }, + { rw div_pos (opow_ne_zero _ hb.ne'), + exact opow_log_le_self b ho } +end + theorem div_opow_log_lt {b : ordinal} (o : ordinal) (hb : 1 < b) : o / b ^ log b o < b := begin rw [div_lt (opow_pos _ (zero_lt_one.trans hb)).ne', ←opow_succ], From c3fcafc76d6c6814076a947261dc7e6b6748c69f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Wed, 1 Mar 2023 03:28:48 -0600 Subject: [PATCH 6/6] Update arithmetic.lean --- src/set_theory/ordinal/arithmetic.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/set_theory/ordinal/arithmetic.lean b/src/set_theory/ordinal/arithmetic.lean index e1eb875801da2..923aee5103745 100644 --- a/src/set_theory/ordinal/arithmetic.lean +++ b/src/set_theory/ordinal/arithmetic.lean @@ -1763,6 +1763,7 @@ end end + /-! ### Casting naturals into ordinals, compatibility with operations -/ @[simp] theorem one_add_nat_cast (m : ℕ) : 1 + (m : ordinal) = succ m :=