Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-03 11:09 8d9e541b

View on Github →

feat(group_theory/group_action): some lemmas about orbits (#2928) also remove the simp attribute unfolding the definition of orbit. Depends on #2924

Estimated changes

modified theorem mul_action.mem_orbit_iff