Mathlib Map

Theorems · Definition · group theory

ConjAct

Type u_3 → Type u_3

A type alias for a group G. ConjAct G acts on G by conjugation

Defined in
Mathlib.GroupTheory.GroupAction.ConjAct
Cited by
79 results in Mathlib
Foundations
Depth 0 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ConjAct.toConjAct · cited by 56ConjAct.toConjActUnitary.conjStarAlgAut · cited by 26Unitary.conjStarAlgAutConjAct.ofConjAct · cited by 17ConjAct.ofConjActMulAut.conjNormal · cited by 9MulAut.conjNormalModularForm.translate · cited by 6ModularForm.translateConjAct.ofConjAct_toConjAct · cited by 4ConjAct.ofConjAct_toConjA…CuspForm.translate · cited by 3CuspForm.translateEquiv.Perm.support_conj_eq_smul_support · cited by 3Perm.support_conj_eq_smul…lipschitzGroup.conjAct_smul_ι_mem_range_ι · cited by 3lipschitzGroup.conjAct_sm…Subgroup.Commensurable.commensurable_conj · cited by 3Commensurable.commensurab…ConjAct.toConjAct_smul · cited by 3ConjAct.toConjAct_smulIsPGroup.center_nontrivial · cited by 2IsPGroup.center_nontrivialcard_comm_eq_card_conjClasses_mul_card · cited by 2card_comm_eq_card_conjCla…unitsCentralizerEquiv · cited by 2unitsCentralizerEquivSubgroup.Normal.conjAct · cited by 2Normal.conjActConjActCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by91

Results whose statement or proof uses this declaration.