mathlib3
b3a0f850 - feat(group_theory/coset): Fintype instance for quotient by the right relation (#13257)

Commit
3 years ago
feat(group_theory/coset): Fintype instance for quotient by the right relation (#13257) This PR adds a fintype instance for the quotient by the right relation. Co-authored-by: Johan Commelin <johan@commelin.net>
Author
Parents
Loading