mathlib3
aac3141e - feat(group_theory/coset): Right cosets are orbits (#16119)

Commit

3 years ago

feat(group_theory/coset): Right cosets are orbits (#16119) This PR adds a few lemma about the orbit of the action of a subgroup of a group on the group.

Author

tb65536

Parents

eaeb4583

mathlib3 aac3141e - feat(group_theory/coset): Right cosets are orbits (#16119)

mathlib3
aac3141e - feat(group_theory/coset): Right cosets are orbits (#16119)