Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-19 09:10 3527e4ad

View on Github →

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.

Estimated changes