basic): add a computable version of quotient_ker_equiv_of_surjective (#7930)

Commit

4 years ago

feat(data/setoid/basic): add a computable version of quotient_ker_equiv_of_surjective (#7930) Perhaps more usefully, this also allows definitional control of the inverse mapping

Author

eric-wieser

Parents

1e43208e

mathlib3 6578f1ce - feat(data/setoid/basic): add a computable version of quotient_ker_equiv_of_surjective (#7930)

mathlib3
6578f1ce - feat(data/setoid/basic): add a computable version of quotient_ker_equiv_of_surjective (#7930)