Mathlib v3 is deprecated. Go to Mathlib v4

Theorem units.one_coe

Modification history

2018-10-01 20:53
algebra/group.lean
feat(data/zmod/quadratic_reciprocity): quadratic reciprocity (#327) …
Deleted units.one_coeView on Github →
2018-08-04 18:47
algebra/group.lean
feat(algebra/ring): units.neg and associated matter
Modified units.one_coeView on Github →
2018-01-14 21:59
algebra/group.lean
feat(algebra/field): more division lemmas
Modified units.one_coeView on Github →
2017-11-06 03:28
algebra/ring.lean
refactor(algebra/module): clean up PR commit
Added units.one_coeView on Github →