mathlib
09597669 - chore(group_theory/quotient_group): open `function`, use `rfl` (#18014)

Commit

3 years ago

chore(group_theory/quotient_group): open `function`, use `rfl` (#18014)

Author

urkud

urkud

Parents

Loading