From 35eba0107e4cc8a52778259bb5392300267bfc29 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 28 Mar 2017 18:49:35 -0700 Subject: [PATCH] chore(library/init/algebra/ring): use `.` notation --- library/init/algebra/ring.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/algebra/ring.lean b/library/init/algebra/ring.lean index a2f60f13f1..02df921b1f 100644 --- a/library/init/algebra/ring.lean +++ b/library/init/algebra/ring.lean @@ -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 -/