From e382f7c2f9e74ff1e603e93ae0f19f3e3f232ac9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 21 Jun 2015 15:58:54 -0700 Subject: [PATCH] refactor(hott/algebra/field): cleanup use same definition used in the standard library. --- hott/algebra/field.hlean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hott/algebra/field.hlean b/hott/algebra/field.hlean index eeb587552..39751c302 100644 --- a/hott/algebra/field.hlean +++ b/hott/algebra/field.hlean @@ -76,7 +76,7 @@ section division_ring -- assume Ha : a = 0, absurd (Ha⁻¹ ▸ one_div_zero) H definition inv_one_eq : 1⁻¹ = (1:A) := - by rewrite [-mul_one, (inv_mul_cancel (ne.symm zero_ne_one))] + by rewrite [-mul_one, (inv_mul_cancel (ne.symm (@zero_ne_one A _)))] definition div_one : a / 1 = a := by rewrite [↑divide, inv_one_eq, mul_one]