mathlib
6ce70381 - feat(group_theory/congruence): add smul and vadd instances (#17834)

Commit

3 years ago

feat(group_theory/congruence): add smul and vadd instances (#17834) These are defined in the obvious way extending under the quotient.

Author

eric-wieser

Parents