chore(data/rat/basic): a few trivial lemmas about rat.denom (#6667)

src/data/rat/basic.lean

@@ -50,6 +50,8 @@ notation `ℚ` := rat
 
 namespace rat
 
+/-- String representation of a rational numbers, used in `has_repr`, `has_to_string`, and
+`has_to_format` instances. -/
 protected def repr : ℚ → string
 | ⟨n, d, _, _⟩ := if d = 1 then _root_.repr n else
   _root_.repr n ++ "/" ++ _root_.repr d
@@ -219,14 +221,17 @@ theorem num_denom' {n d h c} : (⟨n, d, h, c⟩ : ℚ) = n /. d := num_denom.sy
 
 theorem of_int_eq_mk (z : ℤ) : of_int z = z /. 1 := num_denom'
 
+/-- Define a (dependent) function or prove `∀ r : ℚ, p r` by dealing with rational
+numbers of the form `n /. d` with `0 < d` and coprime `n`, `d`. -/
 @[elab_as_eliminator] def {u} num_denom_cases_on {C : ℚ → Sort u}
    : ∀ (a : ℚ) (H : ∀ n d, 0 < d → (int.nat_abs n).coprime d → C (n /. d)), C a
 | ⟨n, d, h, c⟩ H := by rw num_denom'; exact H n d h c
 
+/-- Define a (dependent) function or prove `∀ r : ℚ, p r` by dealing with rational
+numbers of the form `n /. d` with `d ≠ 0`. -/
 @[elab_as_eliminator] def {u} num_denom_cases_on' {C : ℚ → Sort u}
    (a : ℚ) (H : ∀ (n:ℤ) (d:ℕ), d ≠ 0 → C (n /. d)) : C a :=
-num_denom_cases_on a $ λ n d h c,
-H n d $ ne_of_gt h
+num_denom_cases_on a $ λ n d h c, H n d h.ne'
 
 theorem num_dvd (a) {b : ℤ} (b0 : b ≠ 0) : (a /. b).num ∣ a :=
 begin
@@ -248,6 +253,7 @@ begin
   rw [← int.nat_abs_mul, ← int.coe_nat_dvd, int.dvd_nat_abs, ← e], simp
 end
 
+/-- Addition of rational numbers. Use `(+)` instead. -/
 protected def add : ℚ → ℚ → ℚ
 | ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ := mk_pnat (n₁ * d₂ + n₂ * d₁) ⟨d₁ * d₂, mul_pos h₁ h₂⟩
 
@@ -282,8 +288,9 @@ begin
     ... = (a * d + c * b) * (d₁ * d₂)             : by simp [mul_add, mul_comm, mul_left_comm]
 end
 
-protected def neg : ℚ → ℚ
-| ⟨n, d, h, c⟩ := ⟨-n, d, h, by simp [c]⟩
+/-- Negation of rational numbers. Use `-r` instead. -/
+protected def neg (r : ℚ) : ℚ :=
+⟨-r.num, r.denom, r.pos, by simp [r.cop]⟩
 
 instance : has_neg ℚ := ⟨rat.neg⟩
 
@@ -297,6 +304,7 @@ begin
   simp only [neg_mul_eq_neg_mul_symm, congr_arg has_neg.neg h₁]
 end
 
+/-- Multiplication of rational numbers. Use `(*)` instead. -/
 protected def mul : ℚ → ℚ → ℚ
 | ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ := mk_pnat (n₁ * n₂) ⟨d₁ * d₂, mul_pos h₁ h₂⟩
 
@@ -311,6 +319,7 @@ begin
   cc
 end
 
+/-- Inverse rational number. Use `r⁻¹` instead. -/
 protected def inv : ℚ → ℚ
 | ⟨(n+1:ℕ), d, h, c⟩ := ⟨d, n+1, n.succ_pos, c.symm⟩
 | ⟨0, d, h, c⟩ := 0
@@ -457,14 +466,14 @@ theorem sub_def {a b c d : ℤ} (b0 : b ≠ 0) (d0 : d ≠ 0) :
   a /. b - c /. d = (a * d - c * b) /. (b * d) :=
 by simp [b0, d0, sub_eq_add_neg]
 
-@[simp] lemma denom_neg_eq_denom : ∀ q : ℚ, (-q).denom = q.denom
-| ⟨_, d, _, _⟩ := rfl
+@[simp] lemma denom_neg_eq_denom (q : ℚ) : (-q).denom = q.denom := rfl
 
-@[simp] lemma num_neg_eq_neg_num : ∀ q : ℚ, (-q).num = -(q.num)
-| ⟨n, _, _, _⟩ := rfl
+@[simp] lemma num_neg_eq_neg_num (q : ℚ) : (-q).num = -(q.num) := rfl
 
 @[simp] lemma num_zero : rat.num 0 = 0 := rfl
 
+@[simp] lemma denom_zero : rat.denom 0 = 1 := rfl
+
 lemma zero_of_num_zero {q : ℚ} (hq : q.num = 0) : q = 0 :=
 have q = q.num /. q.denom, from num_denom.symm,
 by simpa [hq]
@@ -545,6 +554,20 @@ theorem mk_pnat_denom (n : ℤ) (d : ℕ+) :
   (mk_pnat n d).denom = d / nat.gcd n.nat_abs d :=
 by cases d; refl
 
+theorem mk_pnat_denom_dvd (n : ℤ) (d : ℕ+) :
+  (mk_pnat n d).denom ∣ d.1 :=
+begin
+  rw mk_pnat_denom,
+  apply nat.div_dvd_of_dvd,
+  apply nat.gcd_dvd_right
+end
+
+theorem add_denom_dvd (q₁ q₂ : ℚ) : (q₁ + q₂).denom ∣ q₁.denom * q₂.denom :=
+by { cases q₁, cases q₂, apply mk_pnat_denom_dvd }
+
+theorem mul_denom_dvd (q₁ q₂ : ℚ) : (q₁ * q₂).denom ∣ q₁.denom * q₂.denom :=
+by { cases q₁, cases q₂, apply mk_pnat_denom_dvd }
+
 theorem mul_num (q₁ q₂ : ℚ) : (q₁ * q₂).num =
   (q₁.num * q₂.num) / nat.gcd (q₁.num * q₂.num).nat_abs (q₁.denom * q₂.denom) :=
 by cases q₁; cases q₂; refl

src/data/rat/order.lean

@@ -26,8 +26,8 @@ namespace rat
 variables (a b c : ℚ)
 open_locale rat
 
-protected def nonneg : ℚ → Prop
-| ⟨n, d, h, c⟩ := 0 ≤ n
+/-- A rational number is called nonnegative if its numerator is nonnegative. -/
+protected def nonneg (r : ℚ) : Prop := 0 ≤ r.num
 
 @[simp] theorem mk_nonneg (a : ℤ) {b : ℤ} (h : 0 < b) : (a /. b).nonneg ↔ 0 ≤ a :=
 begin
@@ -77,6 +77,8 @@ or.imp_right neg_nonneg_of_nonpos (le_total 0 n)
 instance decidable_nonneg : decidable (rat.nonneg a) :=
 by cases a; unfold rat.nonneg; apply_instance
 
+/-- Relation `a ≤ b` on `ℚ` defined as `a ≤ b ↔ rat.nonneg (b - a)`. Use `a ≤ b` instead of
+`rat.le a b`. -/
 protected def le (a b : ℚ) := rat.nonneg (b - a)
 
 instance : has_le ℚ := ⟨rat.le⟩