Commit 2022-03-10 21:17 84cbbc98

View on Github →

feat(algebra/group/to_additive + a few more files): make to_additive convert unit to add_unit (#12564) This likely involves removing names that match autogenerated names.

Estimated changes

Modified src/algebra/group/to_additive.lean

Modified src/algebra/group/units.lean

modified theorem is_unit_iff_exists_inv'

modified theorem is_unit_iff_exists_inv

modified theorem is_unit_of_mul_eq_one

Modified src/data/equiv/mul_add.lean

modified theorem coe_to_units

Modified src/group_theory/congruence.lean

modified def con.lift_on_units

Modified src/group_theory/order_of_element.lean