Added doc-strings to lemmas

src/number_theory/pythagorean_triples.lean

@@ -27,10 +27,13 @@ open_locale classical
 /-- Three integers `x`, `y`, and `z` form a Pythagorean triple if `x * x + y * y = z * z`. -/
 def pythagorean_triple (x y z : ℤ) : Prop := x * x + y * y = z * z
 
+/-- Pythagorean triples are interchangable, i.e `x * x + y * y = y * y + x * x = z * z`.
+This comes from additive commutativity -/
 lemma pythagorean_triple_comm {x y z : ℤ} :
  (pythagorean_triple x y z) ↔ (pythagorean_triple y x z) :=
 by { delta pythagorean_triple, rw add_comm }
 
+/-- The zeroth pythagorean triple is zero -/
 lemma pythagorean_triple.zero : pythagorean_triple 0 0 0 :=
 by simp only [pythagorean_triple, zero_mul, zero_add]
 
@@ -47,6 +50,8 @@ lemma symm :
   pythagorean_triple y x z :=
 by rwa [pythagorean_triple_comm]
 
+/-- A triple is still a triple if you multiple each of `x`, `y` and `z`
+by a constant `k` -/
 lemma mul (k : ℤ) : pythagorean_triple (k * x) (k * y) (k * z) :=
 begin
   by_cases hk : k = 0,
@@ -59,6 +64,8 @@ end
 
 omit h
 
+/-- The pythagorean triple `(k*x, k*y, k*z)` is a triple if and only if
+`(x, y, z)` is also a triple  -/
 lemma mul_iff (k : ℤ) (hk : k ≠ 0) :
   pythagorean_triple (k * x) (k * y) (k * z) ↔ pythagorean_triple x y z :=
 begin