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

chore(library/init/algebra/ring): use . notation

Browse source
This commit is contained in:
Leonardo de Moura 2017-03-28 18:49:35 -07:00
parent c4c2d703f6
commit 35eba0107e
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/algebra/ring.lean
View file

@ -47,7 +47,7 @@ lemma zero_ne_one [s: zero_ne_one_class α] : 0 ≠ (1:α) :=
@[simp]
lemma one_ne_zero [s: zero_ne_one_class α] : (1:α) ≠ 0 :=
take h, @zero_ne_one_class.zero_ne_one α s h^.symm
take h, @zero_ne_one_class.zero_ne_one α s h.symm
/- semiring -/