max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(init/algebra/ordered_ring): theorem has two instances

Browse source
This commit is contained in:
Mario Carneiro 2017-09-16 03:20:02 -04:00 • committed by Leonardo de Moura
parent d54c4e11c2
commit d83b9ef3ef
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/algebra/ordered_ring.lean
View file

@ -334,7 +334,7 @@ lemma mul_self_lt_mul_self_iff {a b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a < b
iff.trans (lt_iff_not_ge _ _) $ iff.trans (not_iff_not_of_iff $ mul_self_le_mul_self_iff h2 h1) $
iff.symm (lt_iff_not_ge _ _)
lemma linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero [s : linear_ordered_ring α]
lemma linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero
{a b : α} (h : a * b = 0) : a = 0 ∨ b = 0 :=
match lt_trichotomy 0 a with
| or.inl hlt₁ :=
@ -366,7 +366,7 @@ class linear_ordered_comm_ring (α : Type u) extends linear_ordered_ring α, com
instance linear_ordered_comm_ring.to_integral_domain [s: linear_ordered_comm_ring α] : integral_domain α :=
{s with
eq_zero_or_eq_zero_of_mul_eq_zero := @linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero α _ _ }
eq_zero_or_eq_zero_of_mul_eq_zero := @linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero α _ }
class decidable_linear_ordered_comm_ring (α : Type u) extends linear_ordered_comm_ring α,
decidable_linear_ordered_comm_group α