feat/refactor(library/theories/number_theory/irrational_roots,library/*): show nth roots irrational, and add lots of missing theorems

library/algebra/ring.lean

@@ -326,7 +326,8 @@ theorem eq_zero_or_eq_zero_of_mul_eq_zero {A : Type} [s : no_zero_divisors A] {a
     (H : a * b = 0) :
   a = 0 ∨ b = 0 := !no_zero_divisors.eq_zero_or_eq_zero_of_mul_eq_zero H
 
-structure integral_domain [class] (A : Type) extends comm_ring A, no_zero_divisors A
+structure integral_domain [class] (A : Type) extends comm_ring A, no_zero_divisors A,
+    zero_ne_one_class A
 
 section
   variables [s : integral_domain A] (a b c d e : A)

library/algebra/ring_power.lean

@@ -3,17 +3,57 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jeremy Avigad
 
-Properties of the power operation in an ordered ring.
+Properties of the power operation in an ordered ring or field.
 
 (Right now, this file is just a stub. More soon.)
 -/
-import .group_power
+import .group_power .ordered_field
 open nat
 
 namespace algebra
 
 variable {A : Type}
 
+section semiring
+variable [s : semiring A]
+include s
+
+theorem zero_pow {m : ℕ} (mpos : m > 0) : 0^m = (0 : A) :=
+have h₁ : ∀ m, 0^succ m = (0 : A),
+  from take m, nat.induction_on m
+    (show 0^1 = 0, by rewrite pow_one)
+    (take m, suppose 0^(succ m) = 0,
+      show 0^(succ (succ m)) = 0, from !zero_mul),
+obtain m' (h₂ : m = succ m'), from exists_eq_succ_of_pos mpos,
+show 0^m = 0, by rewrite h₂; apply h₁
+
+end semiring
+
+section integral_domain
+variable [s : integral_domain A]
+include s
+
+theorem eq_zero_of_pow_eq_zero {a : A} {m : ℕ} (H : a^m = 0) : a = 0 :=
+or.elim (eq_zero_or_pos m)
+  (suppose m = 0,
+    by rewrite [`m = 0` at H, pow_zero at H]; apply absurd H (ne.symm zero_ne_one))
+  (suppose m > 0,
+    have h₁ : ∀ m, a^succ m = 0 → a = 0,
+      begin
+        intro m,
+        induction m with m ih,
+          {rewrite pow_one; intros; assumption},
+        rewrite pow_succ,
+        intro H,
+        cases eq_zero_or_eq_zero_of_mul_eq_zero H with h₃ h₄,
+          assumption,
+        exact ih h₄
+      end,
+    obtain m' (h₂ : m = succ m'), from exists_eq_succ_of_pos `m > 0`,
+    show a = 0, by rewrite h₂ at H; apply h₁ m' H)
+
+end integral_domain
+
 section linear_ordered_semiring
 variable [s : linear_ordered_semiring A]
 include s
@@ -27,14 +67,14 @@ end
 
 theorem pow_nonneg_of_nonneg {x : A} (i : ℕ) (H : x ≥ 0) : x^i ≥ 0 :=
 begin
-  induction i with [j, ih],
+  induction i with j ih,
     {show (1 : A) ≥ 0, from le_of_lt zero_lt_one},
     {show x^(succ j) ≥ 0, from mul_nonneg H ih}
 end
 
 theorem pow_le_pow_of_le {x y : A} (i : ℕ) (H₁ : 0 ≤ x) (H₂ : x ≤ y) : x^i ≤ y^i :=
 begin
-  induction i with [i, ih],
+  induction i with i ih,
     {rewrite *pow_zero, apply le.refl},
   rewrite *pow_succ,
   have H : 0 ≤ x^i, from pow_nonneg_of_nonneg i H₁,
@@ -45,8 +85,6 @@ theorem pow_ge_one {x : A} (i : ℕ) (xge1 : x ≥ 1) : x^i ≥ 1 :=
 assert H : x^i ≥ 1^i, from pow_le_pow_of_le i (le_of_lt zero_lt_one) xge1,
 by rewrite one_pow at H; exact H
 
-set_option formatter.hide_full_terms false
-
 theorem pow_gt_one {x : A} {i : ℕ} (xgt1 : x > 1) (ipos : i > 0) : x^i > 1 :=
 assert xpos : x > 0, from lt.trans zero_lt_one xgt1,
 begin
@@ -60,4 +98,31 @@ end
 
 end linear_ordered_semiring
 
+section decidable_linear_ordered_comm_ring
+variable [s : decidable_linear_ordered_comm_ring A]
+include s
+
+theorem abs_pow (a : A) (n : ℕ) : abs (a^n) = abs a^n :=
+begin
+  induction n with n ih,
+    rewrite [*pow_zero, (abs_of_nonneg zero_le_one : abs (1 : A) = 1)],
+  rewrite [*pow_succ, abs_mul, ih]
+end
+
+end decidable_linear_ordered_comm_ring
+
+section discrete_field
+variable [s : discrete_field A]
+include s
+
+theorem div_pow (a : A) {b : A} {n : ℕ} (bnz : b ≠ 0) : (a / b)^n = a^n / b^n :=
+begin
+  induction n with n ih,
+    rewrite [*pow_zero, div_one],
+  have bnnz : b^n ≠ 0, from suppose b^n = 0, bnz (eq_zero_of_pow_eq_zero this),
+  rewrite [*pow_succ, ih, div_mul_div bnz bnnz]
+end
+
+end discrete_field
+
 end algebra

library/data/int/basic.lean

@@ -126,7 +126,7 @@ definition nat_abs (a : ℤ) : ℕ := int.cases_on a function.id succ
 
 theorem nat_abs_of_nat (n : ℕ) : nat_abs n = n := rfl
 
-theorem nat_abs_eq_zero : Π {a : ℤ}, nat_abs a = 0 → a = 0
+theorem eq_zero_of_nat_abs_eq_zero : Π {a : ℤ}, nat_abs a = 0 → a = 0
 | (of_nat m) H := congr_arg of_nat H
 | -[1+ m']   H := absurd H !succ_ne_zero
 
@@ -375,7 +375,7 @@ calc
 
 theorem nat_abs_add_le (a b : ℤ) : nat_abs (a + b) ≤ nat_abs a + nat_abs b :=
 calc
-  nat_abs (a + b) = pabs (repr (a + b)) : nat_abs_eq_pabs_repr 
+  nat_abs (a + b) = pabs (repr (a + b)) : nat_abs_eq_pabs_repr
               ... = pabs (padd (repr a) (repr b)) : pabs_congr !repr_add
               ... ≤ pabs (repr a) + pabs (repr b) : dist_add_add_le_add_dist_dist
               ... = pabs (repr a) + nat_abs b     : nat_abs_eq_pabs_repr
@@ -469,7 +469,7 @@ theorem one_mul (a : ℤ) : 1 * a = a :=
 mul.comm a 1 ▸ mul_one a
 
 private theorem mul_distrib_prep {a1 a2 b1 b2 c1 c2 : ℕ} :
- ((a1+b1)*c1+(a2+b2)*c2, (a1+b1)*c2+(a2+b2)*c1) = 
+ ((a1+b1)*c1+(a2+b2)*c2, (a1+b1)*c2+(a2+b2)*c1) =
  (a1*c1+a2*c2+(b1*c1+b2*c2), a1*c2+a2*c1+(b1*c2+b2*c1)) :=
 by rewrite[+mul.right_distrib] ⬝ (!congr_arg2 !add.comm4 !add.comm4)
 
@@ -494,7 +494,8 @@ theorem zero_ne_one : (0 : int) ≠ 1 :=
 assume H : 0 = 1, !succ_ne_zero (of_nat.inj H)⁻¹
 
 theorem eq_zero_or_eq_zero_of_mul_eq_zero {a b : ℤ} (H : a * b = 0) : a = 0 ∨ b = 0 :=
-or.imp nat_abs_eq_zero nat_abs_eq_zero (eq_zero_or_eq_zero_of_mul_eq_zero (H ▸ (nat_abs_mul a b)⁻¹))
+or.imp eq_zero_of_nat_abs_eq_zero eq_zero_of_nat_abs_eq_zero
+  (eq_zero_or_eq_zero_of_mul_eq_zero (H ▸ (nat_abs_mul a b)⁻¹))
 
 section migrate_algebra
   open [classes] algebra
@@ -517,6 +518,7 @@ section migrate_algebra
     left_distrib   := mul.left_distrib,
     right_distrib  := mul.right_distrib,
     mul_comm       := mul.comm,
+    zero_ne_one    := zero_ne_one,
     eq_zero_or_eq_zero_of_mul_eq_zero := @eq_zero_or_eq_zero_of_mul_eq_zero⦄
 
   local attribute int.integral_domain [instance]
@@ -526,7 +528,7 @@ section migrate_algebra
   notation [priority int.prio] a ∣ b := dvd a b
 
   migrate from algebra with int
-  replacing sub → sub, dvd → dvd
+    replacing sub → sub, dvd → dvd
 end migrate_algebra
 
 /- additional properties -/

library/data/int/div.lean

@@ -581,6 +581,18 @@ decidable.by_cases
     have abs a ∣ a, from abs_dvd_of_dvd !dvd.refl,
     eq.symm (iff.mpr (!div_eq_iff_eq_mul_left `abs a ≠ 0` this) !eq_sign_mul_abs))
 
+theorem le_of_dvd {a b : ℤ} (bpos : b > 0) (H : a ∣ b) : a ≤ b :=
+or.elim !le_or_gt
+  (suppose a ≤ 0, le.trans this (le_of_lt bpos))
+  (suppose a > 0,
+    obtain c (Hc : b = a * c), from exists_eq_mul_right_of_dvd H,
+    have a * c > 0, by rewrite -Hc; exact bpos,
+    have c > 0, from int.pos_of_mul_pos_left this (le_of_lt `a > 0`),
+    show a ≤ b, from calc
+      a     = a * 1 : mul_one
+        ... ≤ a * c : mul_le_mul_of_nonneg_left (add_one_le_of_lt `c > 0`) (le_of_lt `a > 0`)
+        ... = b     : Hc)
+
 /- div and ordering -/
 
 theorem div_mul_le (a : ℤ) {b : ℤ} (H : b ≠ 0) : a div b * b ≤ a :=

library/data/int/gcd.lean

@@ -42,7 +42,7 @@ theorem gcd_abs_abs (a b : ℤ) : gcd (abs a) (abs b) = gcd a b :=
 by rewrite [↑gcd, *nat_abs_abs]
 
 theorem gcd_of_ne_zero (a : ℤ) {b : ℤ} (H : b ≠ 0) : gcd a b = gcd b (abs a mod abs b) :=
-have nat_abs b ≠ nat.zero,        from assume H', H (nat_abs_eq_zero H'),
+have nat_abs b ≠ nat.zero,        from assume H', H (eq_zero_of_nat_abs_eq_zero H'),
 have (#nat nat_abs b > nat.zero), from nat.pos_of_ne_zero this,
 assert nat.gcd (nat_abs a) (nat_abs b) = (#nat nat.gcd (nat_abs b) (nat_abs a mod nat_abs b)),
   from @nat.gcd_of_pos (nat_abs a) (nat_abs b) this,
@@ -284,6 +284,14 @@ calc
          = gcd a b div abs (gcd a b)  : gcd_div !gcd_dvd_left !gcd_dvd_right
      ... = 1                          : by rewrite [abs_of_nonneg !gcd_nonneg, div_self H]
 
+theorem not_coprime_of_dvd_of_dvd {m n d : ℤ} (dgt1 : d > 1) (Hm : d ∣ m) (Hn : d ∣ n) :
+  ¬ coprime m n :=
+assume co : coprime m n,
+assert d ∣ gcd m n, from dvd_gcd Hm Hn,
+have d ∣ 1, by rewrite [↑coprime at co, co at this]; apply this,
+have d ≤ 1, from le_of_dvd dec_trivial this,
+show false, from not_lt_of_ge `d ≤ 1` `d > 1`
+
 theorem exists_coprime {a b : ℤ} (H : gcd a b ≠ 0) :
   exists a' b', coprime a' b' ∧ a = a' * gcd a b ∧ b = b' * gcd a b :=
 have H1 : a = (a div gcd a b) * gcd a b, from (div_mul_cancel !gcd_dvd_left)⁻¹,

library/data/int/order.lean

@@ -267,9 +267,9 @@ section migrate_algebra
 
   definition ge [reducible] (a b : ℤ) := algebra.has_le.ge a b
   definition gt [reducible] (a b : ℤ) := algebra.has_lt.gt a b
-  infix >= := int.ge
-  infix ≥  := int.ge
-  infix >  := int.gt
+  infix [priority int.prio] >= := int.ge
+  infix [priority int.prio] ≥  := int.ge
+  infix [priority int.prio] >  := int.gt
   definition decidable_ge [instance] (a b : ℤ) : decidable (a ≥ b) :=
   show decidable (b ≤ a), from _
   definition decidable_gt [instance] (a b : ℤ) : decidable (a > b) :=
@@ -280,7 +280,7 @@ section migrate_algebra
   definition sign : ℤ → ℤ := algebra.sign
 
   migrate from algebra with int
-  replacing has_le.ge → ge, has_lt.gt → gt, dvd → dvd, sub → sub, min → min, max → max,
+    replacing dvd → dvd, sub → sub, has_le.ge → ge, has_lt.gt → gt, min → min, max → max,
             abs → abs, sign → sign
 
   attribute le.trans ge.trans lt.trans gt.trans [trans]

library/data/int/power.lean

@@ -5,7 +5,7 @@ Author: Jeremy Avigad
 
 The power function on the integers.
 -/
-import data.int.basic data.int.order data.int.div algebra.group_power
+import data.int.basic data.int.order data.int.div algebra.group_power data.nat.power
 
 namespace int
 
@@ -18,13 +18,27 @@ section migrate_algebra
 
   definition pow (a : ℤ) (n : ℕ) : ℤ := algebra.pow a n
   infix [priority int.prio] ^ := pow
+  definition nmul (n : ℕ) (a : ℤ) : ℤ := algebra.nmul n a
+  infix [priority int.prio] `⬝` := nmul
+  definition imul (i : ℤ) (a : ℤ) : ℤ := algebra.imul i a
 
   migrate from algebra with int
-    replacing dvd → dvd, has_le.ge → ge, has_lt.gt → gt, pow → pow
+    replacing dvd → dvd, sub → sub, has_le.ge → ge, has_lt.gt → gt, min → min, max → max,
+            abs → abs, sign → sign, pow → pow, nmul → nmul, imul → imul
     hiding add_pos_of_pos_of_nonneg,  add_pos_of_nonneg_of_pos,
       add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg, le_add_of_nonneg_of_le,
       le_add_of_le_of_nonneg, lt_add_of_nonneg_of_lt, lt_add_of_lt_of_nonneg,
       lt_of_mul_lt_mul_left, lt_of_mul_lt_mul_right, pos_of_mul_pos_left, pos_of_mul_pos_right
 end migrate_algebra
 
+section
+  open nat
+  theorem of_nat_pow (a n : ℕ) : of_nat (a^n) = (of_nat a)^n :=
+  begin
+    induction n with n ih,
+      apply eq.refl,
+    rewrite [pow_succ, nat.pow_succ, of_nat_mul, ih]
+  end
+end
+
 end int

library/data/nat/gcd.lean

@@ -300,6 +300,14 @@ calc
   gcd (m div gcd m n) (n div gcd m n) = gcd m n div gcd m n : gcd_div !gcd_dvd_left !gcd_dvd_right
      ... = 1 : div_self H
 
+theorem not_coprime_of_dvd_of_dvd {m n d : ℕ} (dgt1 : d > 1) (Hm : d ∣ m) (Hn : d ∣ n) :
+  ¬ coprime m n :=
+assume co : coprime m n,
+assert d ∣ gcd m n, from dvd_gcd Hm Hn,
+have d ∣ 1, by rewrite [↑coprime at co, co at this]; apply this,
+have d ≤ 1, from le_of_dvd dec_trivial this,
+show false, from not_lt_of_ge `d ≤ 1` `d > 1`
+
 theorem exists_coprime {m n : ℕ} (H : gcd m n > 0) :
   exists m' n', coprime m' n' ∧ m = m' * gcd m n ∧ n = n' * gcd m n :=
 have H1 : m = (m div gcd m n) * gcd m n, from (div_mul_cancel !gcd_dvd_left)⁻¹,

library/data/nat/parity.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 
 Parity
 -/
-import data.nat.div logic.identities
+import data.nat.power logic.identities
 
 namespace nat
 open decidable
@@ -229,6 +229,32 @@ suppose odd (n * n),
   have even (n * n), from !even_mul_of_even_left this,
   show false, from `odd (n * n)` this
 
+lemma odd_pow {n m} (h : odd n) : odd (n^m) :=
+nat.induction_on m
+  (show odd (n^0), from dec_trivial)
+  (take m, suppose odd (n^m),
+    show odd (n^(m+1)), from odd_mul_of_odd_of_odd h this)
+
+lemma even_pow {n m} (mpos : m > 0) (h : even n) : even (n^m) :=
+have h₁ : ∀ m, even (n^succ m),
+  from take m, nat.induction_on m
+    (show even (n^1), by rewrite pow_one; apply h)
+    (take m, suppose even (n^succ m),
+      show even (n^(succ (succ m))), from !even_mul_of_even_left h),
+obtain m' (h₂ : m = succ m'), from exists_eq_succ_of_pos mpos,
+show even (n^m), by rewrite h₂; apply h₁
+
+lemma odd_of_odd_pow {n m} (mpos : m > 0) (h : odd (n^m)) : odd n :=
+suppose even n,
+have even (n^m), from even_pow mpos this,
+show false, from `odd (n^m)` this
+
+lemma even_of_even_pow {n m} (h : even (n^m)) : even n :=
+by_contradiction
+  (suppose odd n,
+    have odd (n^m), from odd_pow this,
+    show false, from this `even (n^m)`)
+
 lemma eq_of_div2_of_even {n m : nat} : n div 2 = m div 2 → (even n ↔ even m) → n = m :=
 assume h₁ h₂,
  or.elim (em (even n))

library/data/nat/power.lean

@@ -29,6 +29,25 @@ section migrate_algebra
       pow_nonneg_of_nonneg
 end migrate_algebra
 
+theorem eq_zero_of_pow_eq_zero {a m : ℕ} (H : a^m = 0) : a = 0 :=
+or.elim (eq_zero_or_pos m)
+  (suppose m = 0,
+    by rewrite [`m = 0` at H, pow_zero at H]; contradiction)
+  (suppose m > 0,
+    have h₁ : ∀ m, a^succ m = 0 → a = 0,
+      begin
+        intro m,
+        induction m with m ih,
+          {rewrite pow_one; intros; assumption},
+        rewrite pow_succ,
+        intro H,
+        cases eq_zero_or_eq_zero_of_mul_eq_zero H with h₃ h₄,
+          assumption,
+        exact ih h₄
+      end,
+    obtain m' (h₂ : m = succ m'), from exists_eq_succ_of_pos `m > 0`,
+    show a = 0, by rewrite h₂ at H; apply h₁ m' H)
+
 -- generalize to semirings?
 theorem le_pow_self {x : ℕ} (H : x > 1) : ∀ i, i ≤ x^i
 | 0        := !zero_le

library/data/rat/basic.lean

@@ -533,9 +533,12 @@ section migrate_algebra
 
   definition pow (a : ℚ) (n : ℕ) : ℚ := algebra.pow a n
   infix [priority rat.prio] ^ := pow
+  definition nmul (n : ℕ) (a : ℚ) : ℚ := algebra.nmul n a
+  infix [priority rat.prio] `⬝` := nmul
+  definition imul (i : ℤ) (a : ℚ) : ℚ := algebra.imul i a
 
   migrate from algebra with rat
-    replacing sub → rat.sub, divide → divide, dvd → dvd, pow → pow
+    replacing sub → rat.sub, divide → divide, dvd → dvd, pow → pow, nmul → nmul, imul → imul
 
 end migrate_algebra
 
@@ -555,4 +558,11 @@ decidable.by_cases
           by rewrite [Hc, !int.mul_div_cancel_left bnz, mul.comm]),
     iff.mpr (eq_div_iff_mul_eq bnz') H')
 
+theorem of_int_pow (a : ℤ) (n : ℕ) : of_int (a^n) = (of_int a)^n :=
+begin
+  induction n with n ih,
+    apply eq.refl,
+  rewrite [pow_succ, int.pow_succ, of_int_mul, ih]
+end
+
 end rat

library/data/rat/order.lean

@@ -228,7 +228,7 @@ iff.intro
       (suppose a < b, and.left (iff.mp !lt_iff_le_and_ne this))
       (suppose a = b, this ▸ !le.refl))
 
-theorem to_nonneg : a ≥ 0 → nonneg a :=
+private theorem to_nonneg : a ≥ 0 → nonneg a :=
 by intros; rewrite -sub_zero; eassumption
 
 theorem add_le_add_left (H : a ≤ b) (c : ℚ) : c + a ≤ c + b :=
@@ -240,7 +240,7 @@ theorem mul_nonneg (H1 : a ≥ (0 : ℚ)) (H2 : b ≥ (0 : ℚ)) : a * b ≥ (0
 have nonneg (a * b), from nonneg_mul (to_nonneg H1) (to_nonneg H2),
 !sub_zero⁻¹ ▸ this
 
-theorem to_pos : a > 0 → pos a :=
+private theorem to_pos : a > 0 → pos a :=
 by intros; rewrite -sub_zero; eassumption
 
 theorem mul_pos (H1 : a > (0 : ℚ)) (H2 : b > (0 : ℚ)) : a * b > (0 : ℚ) :=
@@ -314,8 +314,9 @@ section migrate_algebra
   definition sign : ℚ → ℚ := algebra.sign
 
   migrate from algebra with rat
-    replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, dvd → dvd,
-              divide → divide, max → max, min → min, abs → abs, sign → sign
+    replacing sub → sub, dvd → dvd, has_le.ge → ge, has_lt.gt → gt,
+              divide → divide, max → max, min → min, abs → abs, sign → sign,
+              nmul → nmul, imul → imul
 
   attribute le.trans lt.trans lt_of_lt_of_le lt_of_le_of_lt ge.trans gt.trans gt_of_gt_of_ge
                    gt_of_ge_of_gt [trans]
@@ -328,6 +329,52 @@ int.induction_on a
   (take b, abs_of_nonneg (!of_nat_nonneg))
   (take b, by rewrite [this, abs_neg, abs_of_nonneg (!of_nat_nonneg)])
 
+section
+  open int
+
+  set_option pp.coercions true
+
+  theorem num_nonneg_of_nonneg {q : ℚ} (H : q ≥ 0) : num q ≥ 0 :=
+  have of_int (num q) ≥ of_int 0,
+    begin
+      rewrite [-mul_denom],
+      apply mul_nonneg H,
+      rewrite [of_int_le_of_int],
+      exact int.le_of_lt !denom_pos
+    end,
+  show num q ≥ 0, from iff.mp !of_int_le_of_int this
+
+  theorem num_pos_of_pos {q : ℚ} (H : q > 0) : num q > 0 :=
+  have of_int (num q) > of_int 0,
+    begin
+      rewrite [-mul_denom],
+      apply mul_pos H,
+      rewrite [of_int_lt_of_int],
+      exact !denom_pos
+    end,
+  show num q > 0, from iff.mp !of_int_lt_of_int this
+
+  theorem num_neg_of_neg {q : ℚ} (H : q < 0) : num q < 0 :=
+  have of_int (num q) < of_int 0,
+    begin
+      rewrite [-mul_denom],
+      apply mul_neg_of_neg_of_pos H,
+      rewrite [of_int_lt_of_int],
+      exact !denom_pos
+    end,
+  show num q < 0, from iff.mp !of_int_lt_of_int this
+
+  theorem num_nonpos_of_nonpos {q : ℚ} (H : q ≤ 0) : num q ≤ 0 :=
+  have of_int (num q) ≤ of_int 0,
+    begin
+      rewrite [-mul_denom],
+      apply mul_nonpos_of_nonpos_of_nonneg H,
+      rewrite [of_int_le_of_int],
+      exact int.le_of_lt !denom_pos
+    end,
+  show num q ≤ 0, from iff.mp !of_int_le_of_int this
+end
+
 definition ubound : ℚ → ℕ := λ a : ℚ, nat.succ (int.nat_abs (num a))
 
 theorem ubound_ge (a : ℚ) : of_nat (ubound a) ≥ a :=

library/data/real/division.lean

@@ -647,7 +647,7 @@ section migrate_algebra
 
   migrate from algebra with real
     replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, abs → abs, sign → sign, dvd → dvd,
-      divide → divide, max → max, min → min
+      divide → divide, max → max, min → min, pow → pow, nmul → nmul, imul → imul
 end migrate_algebra
 
 infix / := divide

library/data/real/order.lean

@@ -1122,9 +1122,15 @@ section migrate_algebra
   infix [priority real.prio] - := real.sub
   definition dvd (a b : ℝ) : Prop := algebra.dvd a b
   notation [priority real.prio] a ∣ b := real.dvd a b
+  definition pow (a : ℝ) (n : ℕ) : ℝ := algebra.pow a n
+  notation [priority real.prio] a^n := real.pow a n
+  definition nmul (n : ℕ) (a : ℝ) : ℝ := algebra.nmul n a
+  infix [priority real.prio] `⬝` := nmul
+  definition imul (i : ℤ) (a : ℝ) : ℝ := algebra.imul i a
 
   migrate from algebra with real
-    replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, dvd → dvd, divide → divide
+    replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, dvd → dvd, divide → divide,
+              pow → pow, nmul → nmul, imul → imul
 
   attribute le.trans lt.trans lt_of_lt_of_le lt_of_le_of_lt ge.trans gt.trans gt_of_gt_of_ge
                    gt_of_ge_of_gt [trans]

library/theories/number_theory/irrational_roots.lean

@@ -0,0 +1,165 @@
+/-
+Copyright (c) 2015 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Jeremy Avigad
+
+A proof that if n > 1 and a > 0, then the nth root of a is irrational, unless a is a perfect nth power.
+-/
+import data.rat .prime_factorization
+open eq.ops
+
+/- First, a textbook proof that sqrt 2 is irrational. -/
+
+section
+  open nat
+
+  theorem sqrt_two_irrational {a b : ℕ} (co : coprime a b) : a^2 ≠ 2 * b^2 :=
+  assume H : a^2 = 2 * b^2,
+  have even (a^2), from even_of_exists (exists.intro _ H),
+  have even a, from even_of_even_pow this,
+  obtain c (aeq : a = 2 * c), from exists_of_even this,
+  have 2 * (2 * c^2) = 2 * b^2, by rewrite [-H, aeq, *pow_two, mul.assoc, mul.left_comm c],
+  have 2 * c^2 = b^2, from eq_of_mul_eq_mul_left dec_trivial this,
+  have even (b^2), from even_of_exists (exists.intro _ (eq.symm this)),
+  have even b, from even_of_even_pow this,
+  have 2 ∣ gcd a b, from dvd_gcd (dvd_of_even `even a`) (dvd_of_even `even b`),
+  have 2 ∣ 1, from co ▸ this,
+  absurd `2 ∣ 1` dec_trivial
+end
+
+/-
+  Replacing 2 by an arbitrary prime and the power 2 by any n ≥ 1 yields the stronger result
+  that the nth root of an integer is irrational, unless the integer is already a perfect nth
+  power.
+-/
+
+section
+  open nat decidable
+
+  theorem root_irrational {a b c n : ℕ} (npos : n > 0) (apos : a > 0) (co : coprime a b)
+      (H : a^n = c * b^n) :
+    b = 1 :=
+  have bpos : b > 0, from pos_of_ne_zero
+    (suppose b = 0,
+      have a^n = 0, by rewrite [H, this, zero_pow npos],
+      assert a = 0, from eq_zero_of_pow_eq_zero this,
+      show false, from ne_of_lt `0 < a` this⁻¹),
+  have H₁ : ∀ p, prime p → ¬ p ∣ b, from
+    take p, suppose prime p, suppose p ∣ b,
+    assert p ∣ b^n, from dvd_pow_of_dvd_of_pos `p ∣ b` `n > 0`,
+    have p ∣ a^n, by rewrite H; apply dvd_mul_of_dvd_right this,
+    have p ∣ a, from dvd_of_prime_of_dvd_pow `prime p` this,
+    have ¬ coprime a b, from not_coprime_of_dvd_of_dvd (gt_one_of_prime `prime p`) `p ∣ a` `p ∣ b`,
+    show false, from this `coprime a b`,
+  have b < 2, from by_contradiction
+    (suppose ¬ b < 2,
+      have b ≥ 2, from le_of_not_gt this,
+      obtain p [primep pdvdb], from exists_prime_and_dvd this,
+      show false, from H₁ p primep pdvdb),
+  show b = 1, from (le.antisymm (le_of_lt_succ `b < 2`) (succ_le_of_lt `b > 0`))
+end
+
+/-
+  Here we state this in terms of the rationals, ℚ. The main difficulty is casting between ℕ, ℤ,
+  and ℚ.
+-/
+
+section
+  open rat int nat decidable
+
+  theorem denom_eq_one_of_pow_eq {q : ℚ} {n : ℕ} {c : ℤ} (npos : n > 0) (H : q^n = c) :
+    denom q = 1 :=
+  let a := num q, b := denom q in
+  have b ≠ 0, from ne_of_gt (denom_pos q),
+  have bnz : b ≠ (0 : ℚ), from assume H, `b ≠ 0` (of_int.inj H),
+  have bnnz : (#rat b^n ≠ 0), from assume bneqz, bnz (eq_zero_of_pow_eq_zero bneqz),
+  have a^n / b^n = c, using bnz, by rewrite [*of_int_pow, -(!div_pow bnz), -eq_num_div_denom, -H],
+  have a^n = c * b^n, from eq.symm (mul_eq_of_eq_div bnnz this⁻¹),
+  have a^n = c * b^n,  -- int version
+    using this, by rewrite [-of_int_pow at this, -of_int_mul at this]; exact of_int.inj this,
+  have (abs a)^n = abs c * (abs b)^n,
+    using this, by rewrite [-int.abs_pow, this, int.abs_mul, int.abs_pow],
+  have H₁ : (nat_abs a)^n = nat_abs c * (nat_abs b)^n,
+    using this,
+      by apply of_nat.inj; rewrite [int.of_nat_mul, +of_nat_pow, +of_nat_nat_abs]; assumption,
+  have H₂ : nat.coprime (nat_abs a) (nat_abs b), from of_nat.inj !coprime_num_denom,
+  have nat_abs b = 1, from
+    by_cases
+      (suppose q = 0, by rewrite this)
+      (suppose q ≠ 0,
+        have a ≠ 0, from suppose a = 0, `q ≠ 0` (by rewrite [eq_num_div_denom, `a = 0`, zero_div]),
+        have nat_abs a ≠ 0, from suppose nat_abs a = 0, `a ≠ 0` (eq_zero_of_nat_abs_eq_zero this),
+        show nat_abs b = 1, from (root_irrational npos (pos_of_ne_zero this) H₂ H₁)),
+  show b = 1, using this, by rewrite [-of_nat_nat_abs_of_nonneg (le_of_lt !denom_pos), this]
+
+  theorem eq_num_pow_of_pow_eq {q : ℚ} {n : ℕ} {c : ℤ} (npos : n > 0) (H : q^n = c) :
+    c = (num q)^n :=
+  have denom q = 1, from denom_eq_one_of_pow_eq npos H,
+  have of_int c = (num q)^n, using this,
+    by rewrite [-H, eq_num_div_denom q at {1}, this, div_one, of_int_pow],
+  show c = (num q)^n , from of_int.inj this
+end
+
+/- As a corollary, for n > 1, the nth root of a prime is irrational. -/
+
+section
+  open nat
+
+  theorem not_eq_pow_of_prime {p n : ℕ} (a : ℕ) (ngt1 : n > 1) (primep : prime p) : p ≠ a^n :=
+  assume peq : p = a^n,
+  have npos : n > 0, from lt.trans dec_trivial ngt1,
+  have pnez : p ≠ 0, from
+    (suppose p = 0,
+      show false,
+        by let H := (pos_of_prime primep); rewrite this at H; exfalso; exact !lt.irrefl H),
+  have agtz : a > 0, from pos_of_ne_zero
+    (suppose a = 0,
+      show false, using npos pnez, by revert peq; rewrite [this, zero_pow npos]; exact pnez),
+  have n * mult p a = 1, from calc
+    n * mult p a = mult p (a^n) : using agtz, by rewrite [mult_pow n agtz primep]
+             ... = mult p p     : peq
+             ... = 1            : mult_self (gt_one_of_prime primep),
+  have n ∣ 1, from dvd_of_mul_right_eq this,
+  have n = 1, from eq_one_of_dvd_one this,
+  show false, using this, by rewrite this at ngt1; exact !lt.irrefl ngt1
+
+  open int rat
+
+  theorem root_prime_irrational {p n : ℕ} {q : ℚ} (qnonneg : q ≥ 0) (ngt1 : n > 1)
+      (primep : prime p) :
+    q^n ≠ p :=
+  have numq : num q ≥ 0, from num_nonneg_of_nonneg qnonneg,
+  have npos : n > 0, from lt.trans dec_trivial ngt1,
+  suppose q^n = p,
+  have p = (num q)^n, from eq_num_pow_of_pow_eq npos this,
+  have p = (nat_abs (num q))^n, using this numq,
+    by apply of_nat.inj; rewrite [this, of_nat_pow, of_nat_nat_abs_of_nonneg numq],
+  show false, from not_eq_pow_of_prime _ ngt1 primep this
+end
+
+/-
+  Thaetetus, who lives in the fourth century BC, is said to have proved the irrationality of square
+  roots up to seventeen. In Chapter 4 of /Why Prove it Again/, John Dawson notes that Thaetetus may
+  have used an approach similar to the one below. (See data/nat/gcd.lean for the key theorem,
+  "div_gcd_eq_div_gcd".)
+-/
+
+section
+  open int
+
+  example {a b c : ℤ} (co : coprime a b) (apos : a > 0) (bpos : b > 0)
+      (H : a * a = c * (b * b)) :
+    b = 1 :=
+  assert H₁ : gcd (c * b) a = gcd c a, from gcd_mul_right_cancel_of_coprime _ (coprime_swap co),
+  have a * a = c * b * b, by rewrite -mul.assoc at H; apply H,
+  have a div (gcd a b) = c * b div gcd (c * b) a, from div_gcd_eq_div_gcd this bpos apos,
+  have a = c * b div gcd c a,
+    using this, by revert this; rewrite [↑coprime at co, co, div_one, H₁]; intros; assumption,
+  have a = b * (c div gcd c a),
+    using this,
+      by revert this; rewrite [mul.comm, !mul_div_assoc !gcd_dvd_left]; intros; assumption,
+  have b ∣ a, from dvd_of_mul_right_eq this⁻¹,
+  have b ∣ gcd a b, from dvd_gcd this !dvd.refl,
+  have b ∣ 1, using this, by rewrite [↑coprime at co, co at this]; apply this,
+  show b = 1, from eq_one_of_dvd_one (le_of_lt bpos) this
+end

library/theories/number_theory/number_theory.md

@@ -4,4 +4,4 @@ theories.number_theory
 * [primes](primes.lean)
 * [bezout](bezout.lean) : Bezout's theorem
 * [prime_factorization](prime_factorization.lean) : prime divisors and multiplicity
-* [square_root_irrational](square_root_irrational.lean) : quadratic surds
+* [irrational_roots](irrational_roots.lean) : irrationality of nth roots

library/theories/number_theory/prime_factorization.lean

@@ -130,6 +130,9 @@ end
 theorem mult_pow_self {p : ℕ} (i : ℕ) (pgt1 : p > 1) : mult p (p^i) = i :=
 by rewrite [-(mul_one (p^i)), mult_pow_mul i pgt1 zero_lt_one, mult_one_right]
 
+theorem mult_self {p : ℕ} (pgt1 : p > 1) : mult p p = 1 :=
+by rewrite [-pow_one p at {2}]; apply mult_pow_self 1 pgt1
+
 theorem le_mult {p i n : ℕ} (pgt1 : p > 1) (npos : n > 0) (pidvd : p^i ∣ n) : i ≤ mult p n :=
 dvd.elim pidvd
   (take m,
@@ -168,6 +171,13 @@ calc
              ... = mult p m + mult p n                          :
                      by rewrite [!mult_pow_mul `p > 1` m'n'pos, multm'n']
 
+theorem mult_pow {p m : ℕ} (n : ℕ) (mpos : m > 0) (primep : prime p) : mult p (m^n) = n * mult p m :=
+begin
+  induction n with n ih,
+    rewrite [pow_zero, mult_one_right, zero_mul],
+  rewrite [pow_succ, mult_mul primep mpos (!pow_pos_of_pos mpos), ih, succ_mul, add.comm]
+end
+
 theorem dvd_of_forall_prime_mult_le {m n : ℕ} (mpos : m > 0)
     (H : ∀ {p}, prime p → mult p m ≤ mult p n) :
   m ∣ n :=
@@ -178,7 +188,7 @@ begin
     {intros, rewrite meq, apply one_dvd},
   have mgt1 : m > 1, from lt_of_le_of_ne (succ_le_of_lt mpos) (ne.symm mneq),
   have mge2 : m ≥ 2, from succ_le_of_lt mgt1,
-  have hpd : ∃ p, prime p ∧ p ∣ m, from ex_prime_and_dvd mge2,
+  have hpd : ∃ p, prime p ∧ p ∣ m, from exists_prime_and_dvd mge2,
   cases hpd with [p, H1],
   cases H1 with [primep, pdvdm],
   intro n,

library/theories/number_theory/primes.lean

@@ -83,7 +83,7 @@ obtain `m ∣ n` (h₅ : ¬ (m = 1 ∨ m = n)), from iff.mp !not_implies_iff_and
 have ¬ m = 1 ∧ ¬ m = n,  from iff.mp !not_or_iff_not_and_not h₅,
 subtype.tag m (and.intro `m ∣ n` this)
 
-theorem ex_dvd_of_not_prime {n : nat} : n ≥ 2 → ¬ prime n → ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n :=
+theorem exists_dvd_of_not_prime {n : nat} : n ≥ 2 → ¬ prime n → ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n :=
 assume h₁ h₂, ex_of_sub (sub_dvd_of_not_prime h₁ h₂)
 
 definition sub_dvd_of_not_prime2 {n : nat} : n ≥ 2 → ¬ prime n → {m | m ∣ n ∧ m ≥ 2 ∧ m < n} :=
@@ -100,7 +100,7 @@ begin
      exact lt_of_le_and_ne m_le_n m_ne_n}
 end
 
-theorem ex_dvd_of_not_prime2 {n : nat} : n ≥ 2 → ¬ prime n → ∃ m, m ∣ n ∧ m ≥ 2 ∧ m < n :=
+theorem exists_dvd_of_not_prime2 {n : nat} : n ≥ 2 → ¬ prime n → ∃ m, m ∣ n ∧ m ≥ 2 ∧ m < n :=
 assume h₁ h₂, ex_of_sub (sub_dvd_of_not_prime2 h₁ h₂)
 
 definition sub_prime_and_dvd {n : nat} : n ≥ 2 → {p | prime p ∧ p ∣ n} :=
@@ -116,7 +116,7 @@ nat.strong_rec_on n
       have p ∣ n, from dvd.trans p_dvd_m m_dvd_n,
       subtype.tag p (and.intro hp this)))
 
-lemma ex_prime_and_dvd {n : nat} : n ≥ 2 → ∃ p, prime p ∧ p ∣ n :=
+lemma exists_prime_and_dvd {n : nat} : n ≥ 2 → ∃ p, prime p ∧ p ∣ n :=
 assume h, ex_of_sub (sub_prime_and_dvd h)
 
 open eq.ops

library/theories/number_theory/square_root_irrational.lean

@@ -1,52 +0,0 @@
-/-
-Copyright (c) 2015 Jeremy Avigad. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Jeremy Avigad
-
-A proof that the square root of an integer is irrational, unless the integer is a perfect square.
--/
-import data.rat
-open nat eq.ops
-
-/- First, a textbook proof that sqrt 2 is irrational. -/
-
-theorem sqrt_two_irrational_aux {a b : ℕ} (co : coprime a b) : a * a ≠ 2 * (b * b) :=
-assume H : a * a = 2 * (b * b),
-have even (a * a), from even_of_exists (exists.intro _ H),
-have even a, from even_of_even_mul_self this,
-obtain c (aeq : a = 2 * c), from exists_of_even this,
-have 2 * (2 * (c * c)) = 2 * (b * b), by rewrite [-H, aeq, mul.assoc, mul.left_comm c],
-have 2 * (c * c) = b * b, from eq_of_mul_eq_mul_left dec_trivial this,
-have even (b * b), from even_of_exists (exists.intro _ (eq.symm this)),
-have even b, from even_of_even_mul_self this,
-have 2 ∣ gcd a b, from dvd_gcd (dvd_of_even `even a`) (dvd_of_even `even b`),
-have 2 ∣ 1, from co ▸ this,
-absurd `2 ∣ 1` dec_trivial
-
-/- Let's state this in terms of rational numbers. The problem is that we now have to mediate between
-   rat, int, and nat. -/
-
-section
-  open rat int
-
-  theorem sqrt_two_irrational (q : ℚ): q^2 ≠ 2 :=
-  suppose q^2 = 2,
-  let a := num q, b := denom q in
-  have b ≠ 0, from ne_of_gt (denom_pos q),
-  assert bnz : b ≠ (0 : ℚ), from assume H, `b ≠ 0` (of_int.inj H),
-  have b * b ≠ (0 : ℚ), from rat.mul_ne_zero bnz bnz,
-  have (a * a) / (b * b) = 2,
-    by rewrite [*of_int_mul, -div_mul_div bnz bnz, -eq_num_div_denom, -this, rat.pow_two],
-  have a * a = 2 * (b * b), from eq.symm (mul_eq_of_eq_div `b * b ≠ (0 : ℚ)` this⁻¹),
-  assert a * a = 2 * (b * b), from of_int.inj this,    -- now in the integers
-  let a' := nat_abs a, b' := nat_abs b in
-  have H : a' * a' = 2 * (b' * b'),
-    begin
-      apply of_nat.inj,
-      rewrite [-+nat_abs_mul, int.of_nat_mul, +of_nat_nat_abs, +int.abs_mul_self],
-      exact this,
-    end,
-  have coprime a b, from !coprime_num_denom,
-  have nat.coprime a' b', from of_nat.inj this,
-  show false, from sqrt_two_irrational_aux this H
-end