Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-04 18:47 1b937197

View on Github →

feat(algebra/ring): units.neg and associated matter

Estimated changes

Modified algebra/group.lean

added theorem nat.units_eq_one

modified theorem units.ext

added theorem units.ext_iff

modified theorem units.inv_coe

modified theorem units.inv_mul

modified theorem units.inv_mul_cancel_left

modified theorem units.inv_mul_cancel_right

modified theorem units.mul_coe

modified theorem units.mul_inv

modified theorem units.mul_inv_cancel_left

modified theorem units.mul_inv_cancel_right

modified theorem units.mul_left_inj

modified theorem units.mul_right_inj

modified theorem units.one_coe

modified theorem units.val_coe

Modified algebra/ordered_group.lean

added theorem units.coe_le_coe

added theorem units.coe_lt_coe

added theorem units.max_coe

added theorem units.min_coe

Modified algebra/ring.lean

modified theorem bit0_eq_two_mul

modified theorem mul_two

Modified data/int/basic.lean

added theorem int.units_eq_one_or

added theorem int.units_nat_abs

Modified ring_theory/localization.lean

added def localization.inv_aux