*): Move pointwise subgroup operations (#17491)

Commit

3 years ago

move(group_theory/group_action/*): Move pointwise subgroup operations (#17491) ... from `group_theory.group_action.basic` to `group_theory.group_action.pointwise`.

References

lean-3.48.0

Author

YaelDillies

Parents

ad3dfaca

mathlib3 f86ad885 - move(group_theory/group_action/*): Move pointwise subgroup operations (#17491)

mathlib3
f86ad885 - move(group_theory/group_action/*): Move pointwise subgroup operations (#17491)