Theorems · Definition · group theory
DomMulAct.stabilizerEquiv_invFun_aux
{α : Type u_1} → {ι : Type u_2} → {f : α → ι} → ((i : ι) → Equiv.Perm { a // f a = i }) → Equiv.Perm αThe invFun component of MulEquiv from MulAction.stabilizer (Perm α) p
to the product of the Equiv.Perm {a | f a = i} (as an Equiv.Perm α).
- Defined in
- Mathlib.GroupTheory.Perm.DomMulAct
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equiv.symmproof · cited by 3,681
- Equiv.Permstatement and proof · cited by 1,375
- DomMulAct.stabilizerEquiv_invFunproof · cited by 2
Cited by1
Results whose statement or proof uses this declaration.
- DomMulAct.stabilizerMulEquivproof · cited by 2