From bc0dbf0809983e7148dd708fb9184ba12c723474 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Mon, 27 Mar 2017 18:43:20 -0400 Subject: [PATCH] feat(library/init/algebra): add zero_ne_one and one_ne_zero to default simp-set --- library/init/algebra/field.lean | 4 ++-- library/init/algebra/ring.lean | 5 +++++ 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/library/init/algebra/field.lean b/library/init/algebra/field.lean index 2aaf7ae773..2906a5428b 100644 --- a/library/init/algebra/field.lean +++ b/library/init/algebra/field.lean @@ -75,8 +75,8 @@ have 0 = (1:α), from eq.symm (by rw [-(mul_one_div_cancel h), this, mul_zero]), absurd this zero_ne_one lemma one_inv_eq : 1⁻¹ = (1:α) := -suffices 1 * 1⁻¹ = (1:α), begin simp at this, assumption end, -mul_inv_cancel (ne.symm (@zero_ne_one α _)) +calc 1⁻¹ = 1 * 1⁻¹ : by rw [one_mul] + ... = (1:α) : by simp local attribute [simp] one_inv_eq diff --git a/library/init/algebra/ring.lean b/library/init/algebra/ring.lean index e25a8055ca..a2f60f13f1 100644 --- a/library/init/algebra/ring.lean +++ b/library/init/algebra/ring.lean @@ -41,9 +41,14 @@ mul_zero_class.mul_zero a class zero_ne_one_class (α : Type u) extends has_zero α, has_one α := (zero_ne_one : 0 ≠ (1:α)) +@[simp] lemma zero_ne_one [s: zero_ne_one_class α] : 0 ≠ (1:α) := @zero_ne_one_class.zero_ne_one α s +@[simp] +lemma one_ne_zero [s: zero_ne_one_class α] : (1:α) ≠ 0 := +take h, @zero_ne_one_class.zero_ne_one α s h^.symm + /- semiring -/ class semiring (α : Type u) extends add_comm_monoid α, monoid α, distrib α, mul_zero_class α