feat(library/algebra/ring): add lemma

2016-01-30 16:34:59 -08:00 · 2016-01-30 16:34:59 -08:00 · c779590517
commit c779590517
parent a7b37d0e09
1 changed files with 4 additions and 0 deletions
--- a/library/algebra/ring.lean
+++ b/library/algebra/ring.lean
@ -272,6 +272,10 @@ section
  theorem mul_self_sub_one_eq : a * a - 1 = (a + 1) * (a - 1) :=
  by simp

+  theorem add_mul_self_eq : (a + b) * (a + b) = a*a + 2*a*b + b*b :=
+  calc (a + b)*(a + b) = a*a + (1+1)*a*b + b*b : by simp
+               ...     = a*a + 2*a*b + b*b     : by rewrite one_add_one_eq_two
+
  theorem dvd_neg_iff_dvd : (a ∣ -b) ↔ (a ∣ b) :=
  iff.intro
    (suppose a ∣ -b,