Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mul_action.orbit_rel.quotient.orbit_mk

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.orbit_mkView on Github →