quotient): Multiplicative version of `zmultiples_quotient_stabilizer_equiv` (#13948)

Commit

3 years ago

feat(data/zmod/quotient): Multiplicative version of `zmultiples_quotient_stabilizer_equiv` (#13948) This PR adds a multiplicative version of `zmultiples_quotient_stabilizer_equiv`.

Author

tb65536

Parents

03da6818

mathlib caa1352a - feat(data/zmod/quotient): Multiplicative version of `zmultiples_quotient_stabilizer_equiv` (#13948)

mathlib
caa1352a - feat(data/zmod/quotient): Multiplicative version of `zmultiples_quotient_stabilizer_equiv` (#13948)