mathlib3
aa812bd1 - chore(group_theory/group_action/basic): split file (#15044)

Commit
3 years ago
chore(group_theory/group_action/basic): split file (#15044) Split the file `group_theory/group_action/basic` to remove the dependency on `group_theory/quotient_group`, moving everything involving quotients to a new file `group_theory/group_action/quotient`.
Author
Parents
Loading