Commit 2021-08-01 21:03 1530d767

View on Github →

feat(group_theory/congruence): add con.lift_on_units etc (#8488) Add a helper function that makes it easier to define a function on units (con.quotient c).

Estimated changes

Modified src/group_theory/congruence.lean

added theorem con.hrec_on₂_coe

added theorem con.induction_on_units

added def con.lift_on_units

added theorem con.lift_on_units_mk

added theorem con.quot_mk_eq_coe

added theorem con.rel_mk