mathlib
1530d767 - feat(group_theory/congruence): add `con.lift_on_units` etc (#8488)

Commit

4 years ago

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)`.

Author

urkud

Parents

9c4dd02d

mathlib 1530d767 - feat(group_theory/congruence): add `con.lift_on_units` etc (#8488)

mathlib
1530d767 - feat(group_theory/congruence): add `con.lift_on_units` etc (#8488)