embedding): group actions apply on the codomain of embeddings (#12798)

Commit

3 years ago

feat(group_theory/group_action/embedding): group actions apply on the codomain of embeddings (#12798)

Author

eric-wieser

Parents