prod` (#10485)

Commit

4 years ago

chore(algebra/module/pi): split out `group_theory/group_action/pi` to match `group_theory/group_action/prod` (#10485) These declarations are copied without modification.

Author

eric-wieser

Parents

ea52ec1f

mathlib3 dabb58bb - chore(algebra/module/pi): split out `group_theory/group_action/pi` to match `group_theory/group_action/prod` (#10485)

mathlib3
dabb58bb - chore(algebra/module/pi): split out `group_theory/group_action/pi` to match `group_theory/group_action/prod` (#10485)