Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-15 12:56 ca5c4b37

View on Github →

feat(group_theory/group_action): add a few instances (#10310)

  • regular and opposite regular actions of a group on itself are transitive;
  • the action of a group on an orbit is transitive.

Estimated changes

deleted theorem mul_action.exists_smul_eq
modified theorem mul_action.orbit_eq_univ