Theorems · Definition
Function.Involutive.toPerm
{α : Sort u_1} → (f : α → α) → Function.Involutive f → Equiv.Perm αConvert an involutive function f to a permutation with toFun = invFun = f.
- Defined in
- Mathlib.Logic.Equiv.Basic
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equiv.Permstatement · cited by 1,375
- Function.Involutivestatement and proof · cited by 103
- Function.Involutive.leftInverseproof · cited by 5
- Function.Involutive.rightInverseproof · cited by 4
Cited by27
Results whose statement or proof uses this declaration.
- Equiv.negproof · cited by 53
- Fin.revPermproof · cited by 25
- Module.reflectionproof · cited by 25
- Equiv.invproof · cited by 23
- starMulEquivproof · cited by 7
- Equiv.boolNotproof · cited by 5
- MeasurableEquiv.ofInvolutiveproof · cited by 4
- Equiv.Perm.starproof · cited by 4
- starMulAutproof · cited by 3
- Cardinal.mk_perm_eq_self_powerproof · cited by 2
- AddConstMap.conjNegproof · cited by 2
- isIrreducible_iff_sUnion_isClosedproof · cited by 2