Markus Himmel
GitHub
parent
626075ca34
commit
bb6bfdba37
3 changed files with 226 additions and 22 deletions
|
|
@ -1,7 +1,7 @@
|
|||
/-
|
||||
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
|
||||
Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Markus Himmel
|
||||
-/
|
||||
prelude
|
||||
import Init.Data.Nat.Dvd
|
||||
|
|
@ -393,7 +393,7 @@ protected theorem dvd_mul {k m n : Nat} : k ∣ m * n ↔ ∃ k₁ k₂, k₁
|
|||
· rintro ⟨k₁, k₂, hk₁, hk₂, rfl⟩
|
||||
exact Nat.mul_dvd_mul hk₁ hk₂
|
||||
|
||||
theorem gcd_mul_dvd_mul_gcd (k m n : Nat) : gcd k (m * n) ∣ gcd k m * gcd k n := by
|
||||
theorem gcd_mul_right_dvd_mul_gcd (k m n : Nat) : gcd k (m * n) ∣ gcd k m * gcd k n := by
|
||||
let ⟨⟨⟨m', hm'⟩, ⟨n', hn'⟩⟩, (h : gcd k (m * n) = m' * n')⟩ :=
|
||||
dvdProdDvdOfDvdProd <| gcd_dvd_right k (m * n)
|
||||
rw [h]
|
||||
|
|
@ -402,6 +402,13 @@ theorem gcd_mul_dvd_mul_gcd (k m n : Nat) : gcd k (m * n) ∣ gcd k m * gcd k n
|
|||
(dvd_gcd (Nat.dvd_trans (Nat.dvd_mul_right m' n') h') hm')
|
||||
(dvd_gcd (Nat.dvd_trans (Nat.dvd_mul_left n' m') h') hn')
|
||||
|
||||
@[deprecated gcd_mul_right_dvd_mul_gcd (since := "2025-04-02")]
|
||||
theorem gcd_mul_dvd_mul_gcd (k m n : Nat) : gcd k (m * n) ∣ gcd k m * gcd k n :=
|
||||
gcd_mul_right_dvd_mul_gcd k m n
|
||||
|
||||
theorem gcd_mul_left_dvd_mul_gcd (k m n : Nat) : gcd (m * n) k ∣ gcd m k * gcd n k := by
|
||||
simpa [gcd_comm, Nat.mul_comm] using gcd_mul_right_dvd_mul_gcd _ _ _
|
||||
|
||||
theorem dvd_gcd_mul_iff_dvd_mul {k n m : Nat} : k ∣ gcd k n * m ↔ k ∣ n * m := by
|
||||
refine ⟨(Nat.dvd_trans · <| Nat.mul_dvd_mul_right (k.gcd_dvd_right n) m), fun ⟨y, hy⟩ ↦ ?_⟩
|
||||
rw [← gcd_mul_right, hy, gcd_mul_left]
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
/-
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
|
||||
Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Markus Himmel
|
||||
-/
|
||||
prelude
|
||||
import Init.Data.Nat.Gcd
|
||||
|
|
@ -10,9 +10,6 @@ import Init.Data.Nat.Lemmas
|
|||
/-!
|
||||
# Lemmas about `Nat.lcm`
|
||||
|
||||
## Future work:
|
||||
Most of the material about `Nat.gcd` from `Init.Data.Nat.Gcd` has analogues for `Nat.lcm`
|
||||
that should be added to this file.
|
||||
-/
|
||||
|
||||
namespace Nat
|
||||
|
|
@ -29,17 +26,36 @@ Examples:
|
|||
-/
|
||||
def lcm (m n : Nat) : Nat := m * n / gcd m n
|
||||
|
||||
theorem lcm_eq_mul_div (m n : Nat) : lcm m n = m * n / gcd m n := rfl
|
||||
|
||||
@[simp] theorem gcd_mul_lcm (m n : Nat) : gcd m n * lcm m n = m * n := by
|
||||
rw [lcm_eq_mul_div,
|
||||
Nat.mul_div_cancel' (Nat.dvd_trans (gcd_dvd_left m n) (Nat.dvd_mul_right m n))]
|
||||
|
||||
@[simp] theorem lcm_mul_gcd (m n : Nat) : lcm m n * gcd m n = m * n := by
|
||||
simp [Nat.mul_comm]
|
||||
|
||||
@[simp] theorem lcm_dvd_mul (m n : Nat) : lcm m n ∣ m * n := ⟨gcd m n, by simp⟩
|
||||
|
||||
@[simp] theorem gcd_dvd_mul (m n : Nat) : gcd m n ∣ m * n := ⟨lcm m n, by simp⟩
|
||||
|
||||
@[simp] theorem lcm_le_mul {m n : Nat} (hm : 0 < m) (hn : 0 < n) : lcm m n ≤ m * n :=
|
||||
le_of_dvd (Nat.mul_pos hm hn) (lcm_dvd_mul _ _)
|
||||
|
||||
@[simp] theorem gcd_le_mul {m n : Nat} (hm : 0 < m) (hn : 0 < n) : gcd m n ≤ m * n :=
|
||||
le_of_dvd (Nat.mul_pos hm hn) (gcd_dvd_mul _ _)
|
||||
|
||||
theorem lcm_comm (m n : Nat) : lcm m n = lcm n m := by
|
||||
rw [lcm, lcm, Nat.mul_comm n m, gcd_comm n m]
|
||||
rw [lcm_eq_mul_div, lcm_eq_mul_div, Nat.mul_comm n m, gcd_comm n m]
|
||||
instance : Std.Commutative lcm := ⟨lcm_comm⟩
|
||||
|
||||
@[simp] theorem lcm_zero_left (m : Nat) : lcm 0 m = 0 := by simp [lcm]
|
||||
@[simp] theorem lcm_zero_left (m : Nat) : lcm 0 m = 0 := by simp [lcm_eq_mul_div]
|
||||
|
||||
@[simp] theorem lcm_zero_right (m : Nat) : lcm m 0 = 0 := by simp [lcm]
|
||||
@[simp] theorem lcm_zero_right (m : Nat) : lcm m 0 = 0 := by simp [lcm_eq_mul_div]
|
||||
|
||||
@[simp] theorem lcm_one_left (m : Nat) : lcm 1 m = m := by simp [lcm]
|
||||
@[simp] theorem lcm_one_left (m : Nat) : lcm 1 m = m := by simp [lcm_eq_mul_div]
|
||||
|
||||
@[simp] theorem lcm_one_right (m : Nat) : lcm m 1 = m := by simp [lcm]
|
||||
@[simp] theorem lcm_one_right (m : Nat) : lcm m 1 = m := by simp [lcm_eq_mul_div]
|
||||
instance : Std.LawfulIdentity lcm 1 where
|
||||
left_id := lcm_one_left
|
||||
right_id := lcm_one_right
|
||||
|
|
@ -47,16 +63,32 @@ instance : Std.LawfulIdentity lcm 1 where
|
|||
@[simp] theorem lcm_self (m : Nat) : lcm m m = m := by
|
||||
match eq_zero_or_pos m with
|
||||
| .inl h => rw [h, lcm_zero_left]
|
||||
| .inr h => simp [lcm, Nat.mul_div_cancel _ h]
|
||||
| .inr h => simp [lcm_eq_mul_div, Nat.mul_div_cancel _ h]
|
||||
instance : Std.IdempotentOp lcm := ⟨lcm_self⟩
|
||||
|
||||
theorem dvd_lcm_left (m n : Nat) : m ∣ lcm m n :=
|
||||
⟨n / gcd m n, by rw [← Nat.mul_div_assoc m (Nat.gcd_dvd_right m n)]; rfl⟩
|
||||
⟨n / gcd m n, by rw [← Nat.mul_div_assoc m (Nat.gcd_dvd_right m n), lcm_eq_mul_div]⟩
|
||||
|
||||
theorem dvd_lcm_right (m n : Nat) : n ∣ lcm m n := lcm_comm n m ▸ dvd_lcm_left n m
|
||||
|
||||
theorem gcd_mul_lcm (m n : Nat) : gcd m n * lcm m n = m * n := by
|
||||
rw [lcm, Nat.mul_div_cancel' (Nat.dvd_trans (gcd_dvd_left m n) (Nat.dvd_mul_right m n))]
|
||||
theorem lcm_ne_zero (hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0 := by
|
||||
intro h
|
||||
have h1 := gcd_mul_lcm m n
|
||||
rw [h, Nat.mul_zero] at h1
|
||||
match mul_eq_zero.1 h1.symm with
|
||||
| .inl hm1 => exact hm hm1
|
||||
| .inr hn1 => exact hn hn1
|
||||
|
||||
theorem lcm_pos : 0 < m → 0 < n → 0 < lcm m n := by
|
||||
simpa [← Nat.pos_iff_ne_zero] using lcm_ne_zero
|
||||
|
||||
theorem le_lcm_left (m : Nat) (hn : 0 < n) : m ≤ lcm m n :=
|
||||
(Nat.eq_zero_or_pos m).elim (by rintro rfl; simp)
|
||||
(fun hm => le_of_dvd (lcm_pos hm hn) (dvd_lcm_left m n))
|
||||
|
||||
theorem le_lcm_right (hm : 0 < m) (n : Nat) : n ≤ lcm m n :=
|
||||
(Nat.eq_zero_or_pos n).elim (by rintro rfl; simp)
|
||||
(fun hn => le_of_dvd (lcm_pos hm hn) (dvd_lcm_right m n))
|
||||
|
||||
theorem lcm_dvd {m n k : Nat} (H1 : m ∣ k) (H2 : n ∣ k) : lcm m n ∣ k := by
|
||||
match eq_zero_or_pos k with
|
||||
|
|
@ -66,6 +98,18 @@ theorem lcm_dvd {m n k : Nat} (H1 : m ∣ k) (H2 : n ∣ k) : lcm m n ∣ k := b
|
|||
rw [gcd_mul_lcm, ← gcd_mul_right, Nat.mul_comm n k]
|
||||
exact dvd_gcd (Nat.mul_dvd_mul_left _ H2) (Nat.mul_dvd_mul_right H1 _)
|
||||
|
||||
theorem lcm_dvd_iff {m n k : Nat} : lcm m n ∣ k ↔ m ∣ k ∧ n ∣ k :=
|
||||
⟨fun h => ⟨Nat.dvd_trans (dvd_lcm_left _ _) h, Nat.dvd_trans (dvd_lcm_right _ _) h⟩,
|
||||
fun ⟨hm, hn⟩ => lcm_dvd hm hn⟩
|
||||
|
||||
theorem lcm_eq_left_iff_dvd : lcm m n = m ↔ n ∣ m := by
|
||||
refine (Nat.eq_zero_or_pos m).elim (by rintro rfl; simp) (fun hm => ?_)
|
||||
rw [lcm_eq_mul_div, Nat.div_eq_iff_eq_mul_left (gcd_pos_of_pos_left _ hm) (gcd_dvd_mul _ _),
|
||||
Nat.mul_left_cancel_iff hm, Eq.comm, gcd_eq_right_iff_dvd]
|
||||
|
||||
theorem lcm_eq_right_iff_dvd : lcm m n = n ↔ m ∣ n := by
|
||||
rw [lcm_comm, lcm_eq_left_iff_dvd]
|
||||
|
||||
theorem lcm_assoc (m n k : Nat) : lcm (lcm m n) k = lcm m (lcm n k) :=
|
||||
Nat.dvd_antisymm
|
||||
(lcm_dvd
|
||||
|
|
@ -78,12 +122,126 @@ Nat.dvd_antisymm
|
|||
(dvd_lcm_right (lcm m n) k)))
|
||||
instance : Std.Associative lcm := ⟨lcm_assoc⟩
|
||||
|
||||
theorem lcm_ne_zero (hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0 := by
|
||||
intro h
|
||||
have h1 := gcd_mul_lcm m n
|
||||
rw [h, Nat.mul_zero] at h1
|
||||
match mul_eq_zero.1 h1.symm with
|
||||
| .inl hm1 => exact hm hm1
|
||||
| .inr hn1 => exact hn hn1
|
||||
theorem lcm_mul_left (m n k : Nat) : lcm (m * n) (m * k) = m * lcm n k := by
|
||||
refine (Nat.eq_zero_or_pos m).elim (by rintro rfl; simp) (fun hm => ?_)
|
||||
rw [lcm_eq_mul_div, gcd_mul_left,
|
||||
Nat.mul_div_assoc _ (Nat.mul_dvd_mul_left _ (gcd_dvd_right _ _)), Nat.mul_div_mul_left _ _ hm,
|
||||
lcm_eq_mul_div, Nat.mul_div_assoc _ (gcd_dvd_right _ _), Nat.mul_assoc]
|
||||
|
||||
theorem lcm_mul_right (m n k : Nat) : lcm (m * n) (k * n) = lcm m k * n := by
|
||||
rw [Nat.mul_comm _ n, Nat.mul_comm _ n, Nat.mul_comm _ n, lcm_mul_left]
|
||||
|
||||
theorem eq_zero_of_lcm_eq_zero (h : lcm m n = 0) : m = 0 ∨ n = 0 := by
|
||||
cases m <;> cases n <;> simp [lcm_ne_zero] at *
|
||||
|
||||
@[simp] theorem lcm_eq_zero_iff : lcm m n = 0 ↔ m = 0 ∨ n = 0 := by
|
||||
cases m <;> cases n <;> simp [lcm_ne_zero] at *
|
||||
|
||||
theorem lcm_eq_iff {n m l : Nat} :
|
||||
lcm n m = l ↔ n ∣ l ∧ m ∣ l ∧ (∀ c, n ∣ c → m ∣ c → l ∣ c) := by
|
||||
refine ⟨?_, fun ⟨hn, hm, hl⟩ => Nat.dvd_antisymm (lcm_dvd hn hm) ?_⟩
|
||||
· rintro rfl
|
||||
exact ⟨dvd_lcm_left _ _, dvd_lcm_right _ _, fun _ => Nat.lcm_dvd⟩
|
||||
· exact hl _ (dvd_lcm_left _ _) (dvd_lcm_right _ _)
|
||||
|
||||
theorem lcm_div {m n k : Nat} (hkm : k ∣ m) (hkn : k ∣ n) : lcm (m / k) (n / k) = lcm m n / k := by
|
||||
refine (Nat.eq_zero_or_pos k).elim (by rintro rfl; simp) (fun hk => lcm_eq_iff.2
|
||||
⟨Nat.div_dvd_div hkm (dvd_lcm_left m n), Nat.div_dvd_div hkn (dvd_lcm_right m n),
|
||||
fun c hc₁ hc₂ => ?_⟩)
|
||||
rw [div_dvd_iff_dvd_mul _ hk] at hc₁ hc₂ ⊢
|
||||
· exact lcm_dvd hc₁ hc₂
|
||||
· exact Nat.dvd_trans hkm (dvd_lcm_left _ _)
|
||||
· exact hkn
|
||||
· exact hkm
|
||||
|
||||
theorem lcm_dvd_lcm_of_dvd_left {m k : Nat} (n : Nat) (h : m ∣ k) : lcm m n ∣ lcm k n :=
|
||||
lcm_dvd (Nat.dvd_trans h (dvd_lcm_left _ _)) (dvd_lcm_right _ _)
|
||||
|
||||
theorem lcm_dvd_lcm_of_dvd_right {m k : Nat} (n : Nat) (h : m ∣ k) : lcm n m ∣ lcm n k :=
|
||||
lcm_dvd (dvd_lcm_left _ _) (Nat.dvd_trans h (dvd_lcm_right _ _))
|
||||
|
||||
theorem lcm_dvd_lcm_mul_left_left (m n k : Nat) : lcm m n ∣ lcm (k * m) n :=
|
||||
lcm_dvd_lcm_of_dvd_left _ (Nat.dvd_mul_left _ _)
|
||||
|
||||
theorem lcm_dvd_lcm_mul_right_left (m n k : Nat) : lcm m n ∣ lcm (m * k) n :=
|
||||
lcm_dvd_lcm_of_dvd_left _ (Nat.dvd_mul_right _ _)
|
||||
|
||||
theorem lcm_dvd_lcm_mul_left_right (m n k : Nat) : lcm m n ∣ lcm m (k * n) :=
|
||||
lcm_dvd_lcm_of_dvd_right _ (Nat.dvd_mul_left _ _)
|
||||
|
||||
theorem lcm_dvd_lcm_mul_right_right (m n k : Nat) : lcm m n ∣ lcm m (n * k) :=
|
||||
lcm_dvd_lcm_of_dvd_right _ (Nat.dvd_mul_right _ _)
|
||||
|
||||
theorem lcm_eq_left {m n : Nat} (h : n ∣ m) : lcm m n = m :=
|
||||
lcm_eq_left_iff_dvd.2 h
|
||||
|
||||
theorem lcm_eq_right {m n : Nat} (h : m ∣ n) : lcm m n = n :=
|
||||
lcm_eq_right_iff_dvd.2 h
|
||||
|
||||
@[simp] theorem lcm_mul_left_left (m n : Nat) : lcm (m * n) n = m * n := by
|
||||
simpa [lcm_eq_iff, Nat.dvd_mul_left] using fun _ h _ => h
|
||||
|
||||
@[simp] theorem lcm_mul_left_right (m n : Nat) : lcm n (m * n) = m * n := by
|
||||
simp [lcm_eq_iff, Nat.dvd_mul_left]
|
||||
|
||||
@[simp] theorem lcm_mul_right_left (m n : Nat) : lcm (n * m) n = n * m := by
|
||||
simpa [lcm_eq_iff, Nat.dvd_mul_right] using fun _ h _ => h
|
||||
|
||||
@[simp] theorem lcm_mul_right_right (m n : Nat) : lcm n (n * m) = n * m := by
|
||||
simp [lcm_eq_iff, Nat.dvd_mul_right]
|
||||
|
||||
@[simp] theorem lcm_lcm_self_right_left (m n : Nat) : lcm m (lcm m n) = lcm m n := by
|
||||
simp [← lcm_assoc]
|
||||
|
||||
@[simp] theorem lcm_lcm_self_right_right (m n : Nat) : lcm m (lcm n m) = lcm m n := by
|
||||
rw [lcm_comm n m, lcm_lcm_self_right_left]
|
||||
|
||||
@[simp] theorem lcm_lcm_self_left_left (m n : Nat) : lcm (lcm m n) m = lcm n m := by
|
||||
simp [lcm_comm]
|
||||
|
||||
@[simp] theorem lcm_lcm_self_left_right (m n : Nat) : lcm (lcm n m) m = lcm n m := by
|
||||
simp [lcm_comm]
|
||||
|
||||
theorem lcm_eq_mul_iff {m n : Nat} : lcm m n = m * n ↔ m = 0 ∨ n = 0 ∨ gcd m n = 1 := by
|
||||
rw [lcm_eq_mul_div, Nat.div_eq_self, Nat.mul_eq_zero, or_assoc]
|
||||
|
||||
@[simp] theorem lcm_eq_one_iff {m n : Nat} : lcm m n = 1 ↔ m = 1 ∧ n = 1 := by
|
||||
refine ⟨fun h => ⟨?_, ?_⟩, by rintro ⟨rfl, rfl⟩; simp⟩ <;>
|
||||
(apply Nat.eq_one_of_dvd_one; simp [← h, dvd_lcm_left, dvd_lcm_right])
|
||||
|
||||
theorem lcm_mul_right_dvd_mul_lcm (k m n : Nat) : lcm k (m * n) ∣ lcm k m * lcm k n :=
|
||||
lcm_dvd (Nat.dvd_mul_left_of_dvd (dvd_lcm_left _ _) _)
|
||||
(Nat.mul_dvd_mul (dvd_lcm_right _ _) (dvd_lcm_right _ _))
|
||||
|
||||
theorem lcm_mul_left_dvd_mul_lcm (k m n : Nat) : lcm (m * n) k ∣ lcm m k * lcm n k := by
|
||||
simpa [lcm_comm, Nat.mul_comm] using lcm_mul_right_dvd_mul_lcm _ _ _
|
||||
|
||||
theorem lcm_dvd_mul_self_left_iff_dvd_mul {k n m : Nat} : lcm k n ∣ k * m ↔ n ∣ k * m :=
|
||||
⟨fun h => Nat.dvd_trans (dvd_lcm_right _ _) h, fun h => lcm_dvd (Nat.dvd_mul_right k m) h⟩
|
||||
|
||||
theorem lcm_dvd_mul_self_right_iff_dvd_mul {k m n : Nat} : lcm n k ∣ m * k ↔ n ∣ m * k := by
|
||||
rw [lcm_comm, Nat.mul_comm m, lcm_dvd_mul_self_left_iff_dvd_mul]
|
||||
|
||||
theorem lcm_mul_right_right_eq_mul_of_lcm_eq_mul {n m k : Nat} (h : lcm n m = n * m) :
|
||||
lcm n (m * k) = lcm n k * m := by
|
||||
rcases lcm_eq_mul_iff.1 h with (rfl|rfl|h) <;> try (simp; done)
|
||||
rw [Nat.mul_comm _ m, lcm_eq_mul_div, gcd_mul_right_right_of_gcd_eq_one h, Nat.mul_comm,
|
||||
Nat.mul_assoc, Nat.mul_comm k, Nat.mul_div_assoc _ (gcd_dvd_mul _ _), lcm_eq_mul_div]
|
||||
|
||||
theorem lcm_mul_left_right_eq_mul_of_lcm_eq_mul {n m k} (h : lcm n m = n * m) :
|
||||
lcm n (k * m) = lcm n k * m := by
|
||||
rw [Nat.mul_comm, lcm_mul_right_right_eq_mul_of_lcm_eq_mul h, Nat.mul_comm]
|
||||
|
||||
theorem lcm_mul_right_left_eq_mul_of_lcm_eq_mul {n m k} (h : lcm n m = n * m) :
|
||||
lcm (n * k) m = n * lcm k m := by
|
||||
rw [lcm_comm, lcm_mul_right_right_eq_mul_of_lcm_eq_mul, lcm_comm, Nat.mul_comm]
|
||||
rwa [lcm_comm, Nat.mul_comm]
|
||||
|
||||
theorem lcm_mul_left_left_eq_mul_of_lcm_eq_mul {n m k} (h : lcm n m = n * m) :
|
||||
lcm (k * n) m = n * lcm k m := by
|
||||
rw [Nat.mul_comm, lcm_mul_right_left_eq_mul_of_lcm_eq_mul h]
|
||||
|
||||
theorem pow_lcm_pow {k n m : Nat} : lcm (n ^ k) (m ^ k) = (lcm n m) ^ k := by
|
||||
rw [lcm_eq_mul_div, pow_gcd_pow, ← Nat.mul_pow, ← Nat.div_pow (gcd_dvd_mul _ _), lcm_eq_mul_div]
|
||||
|
||||
end Nat
|
||||
|
|
|
|||
|
|
@ -532,6 +532,12 @@ protected theorem pos_of_lt_mul_right {a b c : Nat} (h : a < b * c) : 0 < b := b
|
|||
replace h : 0 < b * c := by omega
|
||||
exact Nat.pos_of_mul_pos_right h
|
||||
|
||||
protected theorem mul_dvd_mul_iff_left {a b c : Nat} (h : 0 < a) : a * b ∣ a * c ↔ b ∣ c :=
|
||||
⟨fun ⟨k, hk⟩ => ⟨k, Nat.mul_left_cancel h (Nat.mul_assoc _ _ _ ▸ hk)⟩, Nat.mul_dvd_mul_left _⟩
|
||||
|
||||
protected theorem mul_dvd_mul_iff_right {a b c : Nat} (h : 0 < c) : a * c ∣ b * c ↔ a ∣ b := by
|
||||
rw [Nat.mul_comm _ c, Nat.mul_comm _ c, Nat.mul_dvd_mul_iff_left h]
|
||||
|
||||
/-! ### div/mod -/
|
||||
|
||||
theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
|
||||
|
|
@ -602,6 +608,27 @@ theorem mod_eq_sub (x w : Nat) : x % w = x - w * (x / w) := by
|
|||
conv => rhs; congr; rw [← mod_add_div x w]
|
||||
simp
|
||||
|
||||
theorem div_dvd_div {m n k : Nat} : k ∣ m → m ∣ n → m / k ∣ n / k := by
|
||||
refine (Nat.eq_zero_or_pos k).elim (by rintro rfl; simp) (fun hk => ?_)
|
||||
rintro ⟨a, rfl⟩ ⟨b, rfl⟩
|
||||
rw [Nat.mul_comm, Nat.mul_div_cancel _ hk, Nat.mul_comm, ← Nat.mul_assoc, Nat.mul_div_cancel _ hk]
|
||||
exact Nat.dvd_mul_left a b
|
||||
|
||||
@[simp] theorem div_dvd_iff_dvd_mul {a b c : Nat} (h : b ∣ a) (hb : 0 < b) :
|
||||
a / b ∣ c ↔ a ∣ b * c := by
|
||||
rcases h with ⟨k, rfl⟩
|
||||
rw [Nat.mul_comm, Nat.mul_div_cancel _ hb, Nat.mul_comm, Nat.mul_dvd_mul_iff_left hb]
|
||||
|
||||
theorem div_eq_self {m n : Nat} : m / n = m ↔ m = 0 ∨ n = 1 := by
|
||||
refine ⟨fun h => (Nat.eq_zero_or_pos m).elim Or.inl ?_, fun h => by cases h <;> simp_all⟩
|
||||
refine fun hm => Or.inr ?_
|
||||
rcases Nat.lt_trichotomy n 1 with (hn|hn|hn)
|
||||
· obtain rfl : n = 0 := by rwa [lt_one_iff] at hn
|
||||
obtain rfl : 0 = m := by simpa [Nat.div_zero] using h
|
||||
simp at hm
|
||||
· exact hn
|
||||
· exact False.elim (absurd h (Nat.ne_of_lt (Nat.div_lt_self hm hn)))
|
||||
|
||||
/-! ### pow -/
|
||||
|
||||
theorem pow_succ' {m n : Nat} : m ^ n.succ = m * m ^ n := by
|
||||
|
|
@ -864,6 +891,18 @@ theorem dvd_of_pow_dvd {p k m : Nat} (hk : 1 ≤ k) (hpk : p ^ k ∣ m) : p ∣
|
|||
protected theorem pow_div {x m n : Nat} (h : n ≤ m) (hx : 0 < x) : x ^ m / x ^ n = x ^ (m - n) := by
|
||||
rw [Nat.div_eq_iff_eq_mul_left (Nat.pow_pos hx) (Nat.pow_dvd_pow _ h), Nat.pow_sub_mul_pow _ h]
|
||||
|
||||
protected theorem div_pow {a b c : Nat} (h : a ∣ b) : (b / a) ^ c = b ^ c / a ^ c := by
|
||||
refine (Nat.eq_zero_or_pos c).elim (by rintro rfl; simp) (fun hc => ?_)
|
||||
refine (Nat.eq_zero_or_pos a).elim (by rintro rfl; simp [hc]) (fun ha => ?_)
|
||||
rw [eq_comm, Nat.div_eq_iff_eq_mul_left (Nat.pow_pos ha)
|
||||
((Nat.pow_dvd_pow_iff (Nat.pos_iff_ne_zero.1 hc)).2 h)]
|
||||
clear hc
|
||||
induction c with
|
||||
| zero => simp
|
||||
| succ c ih =>
|
||||
rw [Nat.pow_succ (b / a), Nat.pow_succ a, Nat.mul_comm _ a, Nat.mul_assoc, ← Nat.mul_assoc _ a,
|
||||
Nat.div_mul_cancel h, Nat.mul_comm b, ← Nat.mul_assoc, ← ih, Nat.pow_succ]
|
||||
|
||||
/-! ### shiftLeft and shiftRight -/
|
||||
|
||||
@[simp] theorem shiftLeft_zero : n <<< 0 = n := rfl
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue