doc(data/padics, data/real/cau_seq, algebra): add doc strings, remove unnecessary assumptions

docs/references.bib

@@ -48,6 +48,24 @@ @book {james1999
        URL = {https://doi.org/10.1007/978-1-4471-3994-2},
 }
 
+@inproceedings{lewis2019,
+ author = {Lewis, Robert Y.},
+ title = {A Formal Proof of Hensel\&\#39;s Lemma over the P-adic Integers},
+ booktitle = {Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs},
+ series = {CPP 2019},
+ year = {2019},
+ isbn = {978-1-4503-6222-1},
+ location = {Cascais, Portugal},
+ pages = {15--26},
+ numpages = {12},
+ url = {http://doi.acm.org/10.1145/3293880.3294089},
+ doi = {10.1145/3293880.3294089},
+ acmid = {3294089},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {Hensel\&\#39;s lemma, Lean, formal proof, p-adic},
+}
+
 @book {riehl2017,
    AUTHOR = {Riehl, Emily},
     TITLE = {Category theory in context},

src/algebra/field.lean

@@ -39,7 +39,7 @@ def mk0 (a : α) (ha : a ≠ 0) : units α :=
 @[simp] lemma mk0_coe (u : units α) (h : (u : α) ≠ 0) : mk0 (u : α) h = u :=
 units.ext rfl
 
-@[simp] lemma units.mk0_inj [field α] {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) :
+@[simp] lemma units.mk0_inj {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) :
   units.mk0 a ha = units.mk0 b hb ↔ a = b :=
 ⟨λ h, by injection h, λ h, units.ext h⟩
 
@@ -144,7 +144,7 @@ by rw [field.div_div_eq_div_mul _ hb hc, field.div_div_eq_div_mul _ hc hb, mul_c
 lemma field.div_div_div_cancel_right (a : α) (hb : b ≠ 0) (hc : c ≠ 0) : (a / c) / (b / c) = a / b :=
 by rw [field.div_div_eq_mul_div _ hb hc, div_mul_cancel _ hc]
 
-lemma field.div_mul_div_cancel (a : α) (hb : b ≠ 0) (hc : c ≠ 0) : (a / c) * (c / b) = a / b :=
+lemma div_mul_div_cancel (a : α) (hc : c ≠ 0) : (a / c) * (c / b) = a / b :=
 by rw [← mul_div_assoc, div_mul_cancel _ hc]
 
 lemma div_eq_div_iff (hb : b ≠ 0) (hd : d ≠ 0) : a / b = c / d ↔ a * d = c * b :=
@@ -171,10 +171,6 @@ lemma div_div_div_cancel_right (a b : α) (hc : c ≠ 0) : (a / c) / (b / c) = a
 if b0 : b = 0 then by simp only [b0, div_zero, zero_div] else
 field.div_div_div_cancel_right _ b0 hc
 
-lemma div_mul_div_cancel (a : α) (hb : b ≠ 0) (hc : c ≠ 0) : (a / c) * (c / b) = a / b :=
-if b0 : b = 0 then by simp only [b0, div_zero, mul_zero] else
-field.div_mul_div_cancel _ b0 hc
-
 lemma div_div_cancel (ha : a ≠ 0) : a / (a / b) = b :=
 if b0 : b = 0 then by simp only [b0, div_zero] else
 field.div_div_cancel ha b0

src/algebra/ordered_field.lean

@@ -139,17 +139,17 @@ calc (λx, x * c) '' {r | a ≤ r ∧ r ≤ b } = (λx, x / c) ⁻¹' {r | a ≤
   ... = {r | a * c ≤ r ∧ r ≤ b * c} :
     set.ext $ by simp [le_div_iff, div_le_iff, hc]
 
-instance linear_ordered_field.to_densely_ordered [linear_ordered_field α] : densely_ordered α :=
+instance linear_ordered_field.to_densely_ordered : densely_ordered α :=
 { dense := assume a₁ a₂ h, ⟨(a₁ + a₂) / 2,
   calc a₁ = (a₁ + a₁) / 2 : (add_self_div_two a₁).symm
     ... < (a₁ + a₂) / 2 : div_lt_div_of_lt_of_pos (add_lt_add_left h _) two_pos,
   calc (a₁ + a₂) / 2 < (a₂ + a₂) / 2 : div_lt_div_of_lt_of_pos (add_lt_add_right h _) two_pos
     ... = a₂ : add_self_div_two a₂⟩ }
 
-instance linear_ordered_field.to_no_top_order [linear_ordered_field α] : no_top_order α :=
+instance linear_ordered_field.to_no_top_order : no_top_order α :=
 { no_top := assume a, ⟨a + 1, lt_add_of_le_of_pos (le_refl a) zero_lt_one ⟩ }
 
-instance linear_ordered_field.to_no_bot_order [linear_ordered_field α] : no_bot_order α :=
+instance linear_ordered_field.to_no_bot_order : no_bot_order α :=
 { no_bot := assume a, ⟨a + -1,
     add_lt_of_le_of_neg (le_refl _) (neg_lt_of_neg_lt $ by simp [zero_lt_one]) ⟩ }
 
@@ -181,10 +181,10 @@ namespace nat
 
 variables {α : Type*} [linear_ordered_field α]
 
-lemma inv_pos_of_nat [linear_ordered_field α] {n : ℕ}  : 0 < ((n : α) + 1)⁻¹ :=
+lemma inv_pos_of_nat {n : ℕ} : 0 < ((n : α) + 1)⁻¹ :=
 inv_pos $ add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one
 
-lemma one_div_pos_of_nat [linear_ordered_field α] {n : ℕ} : 0 < 1 / ((n : α) + 1) :=
+lemma one_div_pos_of_nat {n : ℕ} : 0 < 1 / ((n : α) + 1) :=
 by { rw one_div_eq_inv, exact inv_pos_of_nat }
 
 end nat

src/data/padics/hensel.lean

@@ -2,19 +2,39 @@
 Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis
-
-A proof of Hensel's lemma on ℤ_p, roughly following Keith Conrad's writeup:
-http://www.math.uconn.edu/~kconrad/blurbs/gradnumthy/hensel.pdf
 -/
 
 import data.padics.padic_integers data.polynomial topology.metric_space.cau_seq_filter
 import analysis.specific_limits topology.instances.polynomial
-import tactic.basic
+
+/-!
+# Hensel's lemma on ℤ_p
+
+This file proves Hensel's lemma on ℤ_p, roughly following Keith Conrad's writeup:
+http://www.math.uconn.edu/~kconrad/blurbs/gradnumthy/hensel.pdf
+
+Hensel's lemma gives a simple condition for the existence of a root of a polynomial.
+
+The proof and motivation are described in the paper
+[R. Y. Lewis, *A formal proof of Hensel's lemma over the p-adic integers*][lewis2019].
+
+## References
+
+* http://www.math.uconn.edu/~kconrad/blurbs/gradnumthy/hensel.pdf
+* [R. Y. Lewis, *A formal proof of Hensel's lemma over the p-adic integers*][lewis2019]
+* https://en.wikipedia.org/wiki/Hensel%27s_lemma
+
+## Tags
+
+p-adic, p adic, padic, p-adic integer
+-/
 
 noncomputable theory
 
 local attribute [instance] classical.prop_decidable
 
+-- We begin with some general lemmas that are used below in the computation.
+
 lemma padic_polynomial_dist {p : ℕ} [p.prime] (F : polynomial ℤ_[p]) (x y : ℤ_[p]) :
   ∥F.eval x - F.eval y∥ ≤ ∥x - y∥ :=
 let ⟨z, hz⟩ := F.eval_sub_factor x y in calc
@@ -69,6 +89,7 @@ parameters {p : ℕ} [nat.prime p] {F : polynomial ℤ_[p]} {a : ℤ_[p]}
            (hnorm : ∥F.eval a∥ < ∥F.derivative.eval a∥^2) (hnsol : F.eval a ≠ 0)
 include hnorm
 
+/-- `T` is an auxiliary value that is used to control the behavior of the polynomial `F`. -/
 private def T : ℝ := ∥(F.eval a).val / ((F.derivative.eval a).val)^2∥
 
 private lemma deriv_sq_norm_pos : 0 < ∥F.derivative.eval a∥ ^ 2 :=
@@ -101,6 +122,7 @@ private lemma T_pow' (n : ℕ) : T ^ (2 ^ n) < 1 := (T_pow (nat.pow_pos (by norm
 
 private lemma T_pow_nonneg (n : ℕ) : T ^ n ≥ 0 := pow_nonneg (norm_nonneg _) _
 
+/-- We will construct a sequence of elements of ℤ_p satisfying successive values of `ih`. -/
 private def ih (n : ℕ) (z : ℤ_[p]) : Prop :=
 ∥F.derivative.eval z∥ = ∥F.derivative.eval a∥ ∧ ∥F.eval z∥ ≤ ∥F.derivative.eval a∥^2 * T ^ (2^n)
 
@@ -164,7 +186,8 @@ calc ∥F.eval z'∥
 
 set_option eqn_compiler.zeta true
 
--- we need (ih k) in order to construct the value for k+1, otherwise it might not be an integer.
+/-- Given `z : ℤ_[p]` satisfying `ih n z`, construct `z' : ℤ_[p]` satisfying `ih (n+1) z'`. We need
+the hypothesis `ih n z`, since otherwise `z'` is not necessarily an integer. -/
 private def ih_n {n : ℕ} {z : ℤ_[p]} (hz : ih n z) : {z' : ℤ_[p] // ih (n+1) z'} :=
 have h1 : ∥(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)∥ ≤ 1, from calc_norm_le_one hz,
 let z1 : ℤ_[p] := ⟨_, h1⟩,
@@ -261,7 +284,6 @@ private lemma newton_seq_dist_aux (n : ℕ) :
 private lemma newton_seq_dist {n k : ℕ} (hnk : n ≤ k) :
   ∥newton_seq k - newton_seq n∥ ≤ ∥F.derivative.eval a∥ * T^(2^n) :=
 have hex : ∃ m, k = n + m, from exists_eq_add_of_le hnk,
---  ⟨k - n, by rw [←nat.add_sub_assoc hnk, add_comm, nat.add_sub_assoc (le_refl n), nat.sub_self, nat.add_zero]⟩,
 let ⟨_, hex'⟩ := hex in
 by rw hex'; apply newton_seq_dist_aux; assumption
 

src/data/padics/padic_integers.lean

@@ -2,31 +2,64 @@
 Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis, Mario Carneiro
-
-Define the p-adic integers ℤ_p as a subtype of ℚ_p. Construct algebraic structures on ℤ_p.
 -/
 
 import data.padics.padic_numbers ring_theory.ideals data.int.modeq
-import tactic.linarith
+
+/-!
+# p-adic integers
+
+This file defines the p-adic integers ℤ_p as the subtype of ℚ_p with norm ≤ 1. We show that ℤ_p is a
+complete nonarchimedean normed local ring.
+
+## Important definitions
+
+* `padic_int` : the type of p-adic numbers
+
+## Notation
+
+We introduce the notation ℤ_[p] for the p-adic integers.
+
+## Implementation notes
+
+Much, but not all, of this file assumes that `p` is prime. This assumption is inferred automatically
+by taking (prime p) as a type class argument.
+
+Coercions into ℤ_p are set up to work with the `norm_cast` tactic.
+
+## References
+
+* [F. Q. Gouêva, *p-adic numbers*][gouvea1997]
+* [R. Y. Lewis, *A formal proof of Hensel's lemma over the p-adic integers*][lewis2019]
+* https://en.wikipedia.org/wiki/P-adic_number
+
+## Tags
+
+p-adic, p adic, padic, p-adic integer
+-/
 
 open nat padic metric
 noncomputable theory
 local attribute [instance] classical.prop_decidable
 
+/-- The p-adic integers ℤ_p are the p-adic numbers with norm ≤ 1. -/
 def padic_int (p : ℕ) [p.prime] := {x : ℚ_[p] // ∥x∥ ≤ 1}
 notation `ℤ_[`p`]` := padic_int p
 
 namespace padic_int
 variables {p : ℕ} [nat.prime p]
 
+/-- Addition on ℤ_p is inherited from ℚ_p. -/
 def add : ℤ_[p] → ℤ_[p] → ℤ_[p]
 | ⟨x, hx⟩ ⟨y, hy⟩ := ⟨x+y,
     le_trans (padic_norm_e.nonarchimedean _ _) (max_le_iff.2 ⟨hx,hy⟩)⟩
 
+/-- Multiplication on ℤ_p is inherited from ℚ_p. -/
 def mul : ℤ_[p] → ℤ_[p] → ℤ_[p]
 | ⟨x, hx⟩ ⟨y, hy⟩ := ⟨x*y,
     begin rw padic_norm_e.mul, apply mul_le_one; {assumption <|> apply norm_nonneg} end⟩
 
+/-- Negation on ℤ_p is inherited from ℚ_p. -/
 def neg : ℤ_[p] → ℤ_[p]
 | ⟨x, hx⟩ := ⟨-x, by simpa⟩
 
@@ -83,6 +116,8 @@ instance : has_coe ℤ_[p] ℚ_[p] := ⟨subtype.val⟩
 lemma mk_coe : ∀ (k : ℤ_[p]), (⟨↑k, k.2⟩ : ℤ_[p]) = k
 | ⟨_, _⟩ := rfl
 
+/-- The inverse of a p-adic integer with norm equal to 1 is also a p-adic integer. Otherwise, the
+inverse is defined to be 0. -/
 def inv : ℤ_[p] → ℤ_[p]
 | ⟨k, _⟩ := if h : ∥k∥ = 1 then ⟨1/k, by simp [h]⟩ else 0
 

src/data/padics/padic_norm.lean

@@ -33,6 +33,7 @@ by taking (prime p) as a type class argument.
 ## References
 
 * [F. Q. Gouêva, *p-adic numbers*][gouvea1997]
+* [R. Y. Lewis, *A formal proof of Hensel's lemma over the p-adic integers*][lewis2019]
 * https://en.wikipedia.org/wiki/P-adic_number
 
 ## Tags
@@ -264,8 +265,26 @@ namespace padic_norm
 
 section padic_norm
 open padic_val_rat
-variables (p : ℕ) [hp : p.prime]
-include hp
+variables (p : ℕ)
+
+/--
+Unfolds the definition of the p-adic norm of `q` when `q ≠ 0`.
+-/
+@[simp] protected lemma eq_fpow_of_nonzero {q : ℚ} (hq : q ≠ 0) :
+  padic_norm p q = p ^ (-(padic_val_rat p q)) :=
+by simp [hq, padic_norm]
+
+/--
+The p-adic norm is nonnegative.
+-/
+protected lemma nonneg (q : ℚ) : padic_norm p q ≥ 0 :=
+if hq : q = 0 then by simp [hq]
+else
+  begin
+    unfold padic_norm; split_ifs,
+    apply fpow_nonneg_of_nonneg,
+    exact_mod_cast nat.zero_le _
+  end
 
 /--
 The p-adic norm of 0 is 0.
@@ -278,11 +297,13 @@ The p-adic norm of 1 is 1.
 @[simp] protected lemma one : padic_norm p 1 = 1 := by simp [padic_norm]
 
 /--
-Unfolds the definition of the p-adic norm of `q` when `q ≠ 0`.
+The image of `padic_norm p` is {0} ∪ {p^(-n) | n ∈ ℤ}.
 -/
-@[simp] protected lemma eq_fpow_of_nonzero {q : ℚ} (hq : q ≠ 0) :
-  padic_norm p q = p ^ (-(padic_val_rat p q)) :=
-by simp [hq, padic_norm]
+protected theorem image {q : ℚ} (hq : q ≠ 0) : ∃ n : ℤ, padic_norm p q = p ^ (-n) :=
+⟨ (padic_val_rat p q), by simp [padic_norm, hq] ⟩
+
+variable [hp : p.prime]
+include hp
 
 /--
 If `q ≠ 0`, then `padic_norm p q ≠ 0`.
@@ -313,18 +334,6 @@ begin
   exact_mod_cast hp.ne_zero
 end
 
-/--
-The p-adic norm is nonnegative.
--/
-protected lemma nonneg (q : ℚ) : padic_norm p q ≥ 0 :=
-if hq : q = 0 then by simp [hq]
-else
-  begin
-    unfold padic_norm; split_ifs,
-    apply fpow_nonneg_of_nonneg,
-    exact_mod_cast nat.zero_le _
-  end
-
 /--
 The p-adic norm is multiplicative.
 -/
@@ -438,12 +447,6 @@ begin
     assumption }
 end
 
-/--
-The image of `padic_norm p` is {0} ∪ {p^(-n) | n ∈ ℤ}.
--/
-protected theorem image {q : ℚ} (hq : q ≠ 0) : ∃ n : ℤ, padic_norm p q = p ^ (-n) :=
-⟨ (padic_val_rat p q), by simp [padic_norm, hq] ⟩
-
 /--
 The p-adic norm is an absolute value: positive-definite and multiplicative, satisfying the triangle
 inequality.