Theorems · Theorem · group theory
ConjAct.ofConjAct_toConjAct
∀ {G : Type u_3} [inst : DivInvMonoid G] (x : G), ConjAct.ofConjAct (ConjAct.toConjAct x) = x- Defined in
- Mathlib.GroupTheory.GroupAction.ConjAct
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses Quot.sound
- Assumes
- DivInvMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- MulEquivstatement · cited by 1,142
- DivInvMonoidstatement and proof · cited by 103
- ConjActstatement · cited by 79
- ConjAct.toConjActstatement · cited by 56
- ConjAct.ofConjActstatement · cited by 17
Cited by4
Results whose statement or proof uses this declaration.
- lipschitzGroup.conjAct_smul_ι_mem_range_ιproof · cited by 3
- Equiv.Perm.support_toConjAct_eq_smul_supportproof · cited by 1
- spinGroup.units_involute_act_eq_conjActproof · cited by 0
- Equiv.Perm.cycleFactorsFinset_conjproof · cited by 0