Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-30 14:55 d2451658

View on Github →

refactor(algebra): add more facts about units

Estimated changes

Modified algebra/field.lean

deleted theorem units.ne_zero

Modified algebra/group.lean

added def units.mk_of_mul_eq_one

Modified algebra/ring.lean

added theorem units.coe_dvd

added theorem units.coe_mul_dvd

added theorem units.dvd_coe

added theorem units.dvd_coe_mul

added theorem units.ne_zero

added theorem zero_dvd_iff_eq_zero