mathlib

3527e4ad - refactor(group_theory/group_action/basic): Make `mul_action.self_equiv_sigma_orbits` computable (#14591)

refactor(group_theory/group_action/basic): Make `mul_action.self_equiv_sigma_orbits` computable (#14591) This introduces a new `mul_action.orbit_rel.quotient.orbit` definition to avoid the need for `.out`.