Mathlib v3 is deprecated. Go to Mathlib v4

Def mul_action.orbit_rel.quotient

Modification history

2022-07-19 09:10

src/group_theory/group_action/basic.lean

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

Added mul_action.orbit_rel.quotient View on Github →