feat(Rat): Numerator and denominator of q ^ n (#12506)

Prove `(q ^ n).num = q.num ^ n` and `(q ^ n).den = q.den ^ n` by making those defeq. It is somewhat painful. `(q ^ n).den = q.den ^ n` is also defeq for `NNRat`, but not `(q ^ n).num = q.num ^ n` due to the `Int.natAbs` in the definition of `NNRat.num`.




Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: YaelDillies

Mathlib/Data/NNRat/Defs.lean

@@ -121,6 +121,12 @@ theorem coe_mul (p q : ℚ≥0) : ((p * q : ℚ≥0) : ℚ) = p * q :=
   rfl
 #align nnrat.coe_mul NNRat.coe_mul
 
+@[simp, norm_cast] lemma coe_pow (q : ℚ≥0) (n : ℕ) : (↑(q ^ n) : ℚ) = (q : ℚ) ^ n := rfl
+#align nnrat.coe_pow NNRat.coe_pow
+
+@[simp] lemma num_pow (q : ℚ≥0) (n : ℕ) : (q ^ n).num = q.num ^ n := by simp [num, Int.natAbs_pow]
+@[simp] lemma den_pow (q : ℚ≥0) (n : ℕ) : (q ^ n).den = q.den ^ n := rfl
+
 -- Porting note: `bit0` `bit1` are deprecated, so remove these theorems.
 #noalign nnrat.coe_bit0
 #noalign nnrat.coe_bit1
@@ -202,10 +208,6 @@ theorem coe_coeHom : ⇑coeHom = ((↑) : ℚ≥0 → ℚ) :=
   rfl
 #align nnrat.coe_coe_hom NNRat.coe_coeHom
 
-@[simp, norm_cast]
-theorem coe_pow (q : ℚ≥0) (n : ℕ) : (↑(q ^ n) : ℚ) = (q : ℚ) ^ n :=
-  coeHom.map_pow _ _
-#align nnrat.coe_pow NNRat.coe_pow
 @[norm_cast]
 theorem nsmul_coe (q : ℚ≥0) (n : ℕ) : ↑(n • q) = n • (q : ℚ) :=
   coeHom.toAddMonoidHom.map_nsmul _ _

Mathlib/Data/Rat/Defs.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Algebra.Ring.Basic
-import Mathlib.Algebra.GroupWithZero.Basic
+import Mathlib.Algebra.GroupWithZero.Units.Basic
 import Mathlib.Algebra.Order.Ring.Int
 import Mathlib.Data.Int.Cast.Defs
 import Mathlib.Data.Rat.Init
@@ -44,6 +44,8 @@ theorem pos (a : ℚ) : 0 < a.den := Nat.pos_of_ne_zero a.den_nz
 
 #align rat.of_int Rat.ofInt
 
+lemma mk'_num_den (q : ℚ) : mk' q.num q.den q.den_nz q.reduced = q := rfl
+
 @[simp]
 theorem ofInt_eq_cast (n : ℤ) : ofInt n = Int.cast n :=
   rfl
@@ -218,6 +220,12 @@ lemma divInt_mul_divInt' (n₁ d₁ n₂ d₂ : ℤ) : (n₁ /. d₁) * (n₂ /.
 
 attribute [simp] mkRat_mul_mkRat
 
+lemma mk'_mul_mk' (n₁ n₂ : ℤ) (d₁ d₂ : ℕ) (hd₁ hd₂ hnd₁ hnd₂) (h₁₂ : n₁.natAbs.Coprime d₂)
+    (h₂₁ : n₂.natAbs.Coprime d₁) :
+    mk' n₁ d₁ hd₁ hnd₁ * mk' n₂ d₂ hd₂ hnd₂ = mk' (n₁ * n₂) (d₁ * d₂) (Nat.mul_ne_zero hd₁ hd₂) (by
+      rw [Int.natAbs_mul]; exact (hnd₁.mul h₂₁).mul_right (h₁₂.mul hnd₂)) := by
+  rw [mul_def]; dsimp; rw [mk_eq_normalize]
+
 lemma mul_eq_mkRat (q r : ℚ) : q * r = mkRat (q.num * r.num) (q.den * r.den) := by
   rw [mul_def, normalize_eq_mkRat]
 
@@ -227,6 +235,28 @@ alias divInt_eq_divInt := divInt_eq_iff
 @[deprecated] alias mul_num_den := mul_eq_mkRat
 #align rat.mul_num_denom Rat.mul_eq_mkRat
 
+instance instPowNat : Pow ℚ ℕ where
+  pow q n := ⟨q.num ^ n, q.den ^ n, by simp [Nat.pow_eq_zero], by
+    rw [Int.natAbs_pow]; exact q.reduced.pow _ _⟩
+
+lemma pow_def (q : ℚ) (n : ℕ) :
+    q ^ n = ⟨q.num ^ n, q.den ^ n,
+      by simp [Nat.pow_eq_zero],
+      by rw [Int.natAbs_pow]; exact q.reduced.pow _ _⟩ := rfl
+
+lemma pow_eq_mkRat (q : ℚ) (n : ℕ) : q ^ n = mkRat (q.num ^ n) (q.den ^ n) := by
+  rw [pow_def, mk_eq_mkRat]
+
+lemma pow_eq_divInt (q : ℚ) (n : ℕ) : q ^ n = q.num ^ n /. q.den ^ n := by
+  rw [pow_def, mk_eq_divInt, Int.natCast_pow]
+
+@[simp] lemma num_pow (q : ℚ) (n : ℕ) : (q ^ n).num = q.num ^ n := rfl
+@[simp] lemma den_pow (q : ℚ) (n : ℕ) : (q ^ n).den = q.den ^ n := rfl
+
+@[simp] lemma mk'_pow (num : ℤ) (den : ℕ) (hd hdn) (n : ℕ) :
+    mk' num den hd hdn ^ n = mk' (num ^ n) (den ^ n)
+      (by simp [Nat.pow_eq_zero, hd]) (by rw [Int.natAbs_pow]; exact hdn.pow _ _) := rfl
+
 #align rat.inv Rat.inv
 
 instance : Inv ℚ :=
@@ -350,6 +380,16 @@ instance commRing : CommRing ℚ where
   one_mul := Rat.one_mul
   mul_comm := Rat.mul_comm
   mul_assoc := Rat.mul_assoc
+  npow n q := q ^ n
+  npow_zero := by intros; apply Rat.ext <;> simp
+  npow_succ n q := by
+    dsimp
+    rw [← q.mk'_num_den, mk'_pow, mk'_mul_mk']
+    congr
+    · rw [mk'_pow, Int.natAbs_pow]
+      exact q.reduced.pow_left _
+    · rw [mk'_pow]
+      exact q.reduced.pow_right _
   zero_mul := Rat.zero_mul
   mul_zero := Rat.mul_zero
   left_distrib := Rat.mul_add
@@ -481,6 +521,9 @@ protected theorem add_divInt (a b c : ℤ) : (a + b) /. c = a /. c + b /. c :=
 theorem divInt_eq_div (n d : ℤ) : n /. d = (n : ℚ) / d := by simp [div_def']
 #align rat.mk_eq_div Rat.divInt_eq_div
 
+lemma intCast_div_eq_divInt (n d : ℤ) : (n : ℚ) / (d) = n /. d := by rw [divInt_eq_div]
+#align rat.coe_int_div_eq_mk Rat.intCast_div_eq_divInt
+
 theorem divInt_mul_divInt_cancel {x : ℤ} (hx : x ≠ 0) (n d : ℤ) : n /. x * (x /. d) = n /. d := by
   by_cases hd : d = 0
   · rw [hd]
@@ -498,16 +541,17 @@ theorem divInt_div_divInt_cancel_right {x : ℤ} (hx : x ≠ 0) (n d : ℤ) :
   rw [div_eq_mul_inv, inv_divInt', mul_comm, divInt_mul_divInt_cancel hx]
 #align rat.mk_div_mk_cancel_right Rat.divInt_div_divInt_cancel_right
 
-theorem intCast_div_eq_divInt {n d : ℤ} : (n : ℚ) / (d) = n /. d := by
-  repeat rw [intCast_eq_divInt]
-  exact divInt_div_divInt_cancel_left one_ne_zero n d
-#align rat.coe_int_div_eq_mk Rat.intCast_div_eq_divInt
-
 -- Porting note: see porting note above about `Int.cast`@[simp]
 theorem num_div_den (r : ℚ) : (r.num : ℚ) / (r.den : ℚ) = r := by
   rw [← Int.cast_natCast]; erw [← divInt_eq_div, num_divInt_den]
 #align rat.num_div_denom Rat.num_div_den
 
+@[simp] lemma divInt_pow (num : ℕ) (den : ℤ) (n : ℕ) : (num /. den) ^ n = num ^ n /. den ^ n := by
+  simp [divInt_eq_div, div_pow]
+
+@[simp] lemma mkRat_pow (num den : ℕ) (n : ℕ) : mkRat num den ^ n = mkRat (num ^ n) (den ^ n) := by
+  rw [mkRat_eq_divInt, mkRat_eq_divInt, divInt_pow, Int.natCast_pow]
+
 theorem coe_int_num_of_den_eq_one {q : ℚ} (hq : q.den = 1) : (q.num : ℚ) = q := by
   conv_rhs => rw [← num_divInt_den q, hq]
   rw [intCast_eq_divInt]

Mathlib/NumberTheory/DiophantineApproximation.lean

@@ -156,7 +156,7 @@ theorem exists_rat_abs_sub_le_and_den_le (ξ : ℝ) {n : ℕ} (n_pos : 0 < n) :
   have hk₀' : (0 : ℝ) < k := Int.cast_pos.mpr hk₀
   have hden : ((j / k : ℚ).den : ℤ) ≤ k := by
     convert le_of_dvd hk₀ (Rat.den_dvd j k)
-    exact Rat.intCast_div_eq_divInt
+    exact Rat.intCast_div_eq_divInt _ _
   refine' ⟨j / k, _, Nat.cast_le.mp (hden.trans hk₁)⟩
   rw [← div_div, le_div_iff (Nat.cast_pos.mpr <| Rat.pos _ : (0 : ℝ) < _)]
   refine' (mul_le_mul_of_nonneg_left (Int.cast_le.mpr hden : _ ≤ (k : ℝ)) (abs_nonneg _)).trans _