michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(hott/algebra/field): cleanup

Browse source 
use same definition used in the standard library.
This commit is contained in:
Leonardo de Moura 2015-06-21 15:58:54 -07:00
parent e3062c64e2
commit e382f7c2f9
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/algebra/field.hlean
View file

@ -76,7 +76,7 @@ section division_ring
-- assume Ha : a = 0, absurd (Ha⁻¹ ▸ one_div_zero) H -- assume Ha : a = 0, absurd (Ha⁻¹ ▸ one_div_zero) H
definition inv_one_eq : 1⁻¹ = (1:A) := 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 := definition div_one : a / 1 = a :=
by rewrite [↑divide, inv_one_eq, mul_one] by rewrite [↑divide, inv_one_eq, mul_one]