mathlib3
6ee5a076 - chore(group_theory/semidirect_product): don't use private defs (#17290)

Commit

3 years ago

chore(group_theory/semidirect_product): don't use private defs (#17290)

Author

urkud

urkud

Parents

Loading