ConjAct

📁 Source: Mathlib/GroupTheory/GroupAction/ConjAct.lean

Statistics

Metric	Count
Definitions conjAction, conjMulDistribMulAction, instDivInvMonoid, instFintype, instGroup, instInhabited, instMulDistribMulAction, instSMul, ofConjAct, rec, toConjAct, unitsMulDistribMulAction, unitsScalar, conjNormal, unitsCentralizerEquiv	15
Theorems val_conj_smul, card, fixedPoints_eq_center, forall, mem_orbit_conjAct, normal_of_characteristic_of_normal, ofConjAct_inv, ofConjAct_mul, ofConjAct_one, ofConjAct_toConjAct, of_mul_symm_eq, orbitRel_conjAct, orbit_eq_carrier_conjClasses, smulCommClass, smulCommClass', smul_def, smul_eq_mulAut_conj, stabilizer_eq_centralizer, toConjAct_inv, toConjAct_mul, toConjAct_ofConjAct, toConjAct_one, toConjAct_smul, to_mul_symm_eq, unitsSMulCommClass, unitsSMulCommClass', units_smul_def, conjNormal_apply, conjNormal_inv_apply, conjNormal_symm_apply, conjNormal_val, centralizer_eq_comap_stabilizer, val_unitsCentralizerEquiv_apply_coe, val_unitsCentralizerEquiv_symm_apply_coe	34
Total	49

ConjAct

Definitions

Name	Category	Theorems
instDivInvMonoid 📖	CompOp	54 math math: smul_def, fixedPoints_eq_center, toConjAct_inv, toConjAct_mul, stabilizer_eq_centralizer, CongruenceSubgroup.exists_Gamma_le_conj', CongruenceSubgroup.conjGL_coe, forall, IsCusp.of_isFiniteRelIndex_conj, toConjAct_zero, SlashInvariantForm.coe_translate, Subgroup.Normal.conjAct, Subgroup.Commensurable.commensurable_conj, Subgroup.conjAct_pointwise_smul_iff, lipschitzGroup.conjAct_smul_ι_mem_range_ι, spinGroup.units_involute_act_eq_conjAct, Subgroup.Commensurable.commensurator_mem_iff, spinGroup.conjAct_smul_ι_mem_range_ι, spinGroup.conjAct_smul_range_ι, ofConjAct_zero, CongruenceSubgroup.IsArithmetic.conj, CongruenceSubgroup.Gamma_cong_eq_self, units_smul_def, Subgroup.normalCore_eq_iInf_conjAct, CongruenceSubgroup.isArithmetic_conj_SL2Z, of_mul_symm_eq, pinGroup.conjAct_smul_ι_mem_range_ι, CuspForm.coe_translate, Unitary.toAlgEquiv_conjStarAlgAut, toConjAct_smul, pinGroup.conjAct_smul_range_ι, val_unitsCentralizerEquiv_symm_apply_coe, Subgroup.Commensurable.commensurable_inv, Unitary.toRingEquiv_conjStarAlgAut, Subgroup.Commensurable.conj, ofConjAct_toConjAct, Equiv.Perm.OnCycleFactors.Subgroup.Centralizer.toConjAct_smul_mem_cycleFactorsFinset, Subgroup.conjAct_pointwise_smul_eq_self, Subgroup.Commensurable.commensurator'_mem_iff, Equiv.Perm.cycleFactorsFinset_conj, CongruenceSubgroup.conj_cong_is_cong, ofConjAct_mul, ofConjAct_inv, to_mul_symm_eq, ModularForm.coe_translate, Equiv.Perm.mem_conj_support, toConjAct_ofConjAct, toConjAct_one, ofConjAct_one, Subgroup.IsArithmetic.conj, lipschitzGroup.conjAct_smul_range_ι, IsCusp.smul, smul_eq_mulAut_conj, Subgroup.centralizer_eq_comap_stabilizer
instFintype 📖	CompOp	1 math math: card
instGroup 📖	CompOp	13 math math: stabilizer_eq_centralizer, val_unitsCentralizerEquiv_apply_coe, Unitary.toAlgEquiv_conjStarAlgAut, val_unitsCentralizerEquiv_symm_apply_coe, Subgroup.Commensurable.commensurable_inv, Unitary.toRingEquiv_conjStarAlgAut, Subgroup.Commensurable.commensurator'_mem_iff, Module.End.mulSemiringActionToAlgEquiv_conjAct_surjective, orbitRel_conjAct, Equiv.Perm.mem_conj_support, ConjClasses.card_carrier, Subgroup.nat_card_centralizer_nat_card_stabilizer, Subgroup.centralizer_eq_comap_stabilizer
instInhabited 📖	CompOp	—
instMulDistribMulAction 📖	CompOp	29 math math: fixedPoints_eq_center, stabilizer_eq_centralizer, CongruenceSubgroup.exists_Gamma_le_conj', CongruenceSubgroup.conjGL_coe, val_unitsCentralizerEquiv_apply_coe, IsCusp.of_isFiniteRelIndex_conj, SlashInvariantForm.coe_translate, Subgroup.Normal.conjAct, Subgroup.Commensurable.commensurable_conj, Subgroup.conjAct_pointwise_smul_iff, Subgroup.Commensurable.commensurator_mem_iff, CongruenceSubgroup.IsArithmetic.conj, CongruenceSubgroup.Gamma_cong_eq_self, Subgroup.normalCore_eq_iInf_conjAct, CongruenceSubgroup.isArithmetic_conj_SL2Z, CuspForm.coe_translate, val_unitsCentralizerEquiv_symm_apply_coe, Subgroup.Commensurable.commensurable_inv, Subgroup.Commensurable.conj, Subgroup.conjAct_pointwise_smul_eq_self, Subgroup.Commensurable.commensurator'_mem_iff, CongruenceSubgroup.conj_cong_is_cong, orbitRel_conjAct, ModularForm.coe_translate, ConjClasses.card_carrier, Subgroup.nat_card_centralizer_nat_card_stabilizer, Subgroup.IsArithmetic.conj, IsCusp.smul, Subgroup.centralizer_eq_comap_stabilizer
instSMul 📖	CompOp	15 math math: smul_def, smulCommClass₀, smulCommClass₀', smulCommClass', smulCommClass, toConjAct_smul, Equiv.Perm.mem_cycleFactorsFinset_conj', Equiv.Perm.OnCycleFactors.Subgroup.Centralizer.toConjAct_smul_mem_cycleFactorsFinset, Subgroup.val_conj_smul, Equiv.Perm.cycleFactorsFinset_conj_eq, mem_orbit_conjAct, Equiv.Perm.cycleFactorsFinset_conj, orbit_eq_carrier_conjClasses, Equiv.Perm.mem_conj_support, smul_eq_mulAut_conj
ofConjAct 📖	CompOp	13 math math: smul_def, ofConjAct_zero, units_smul_def, of_mul_symm_eq, val_unitsCentralizerEquiv_symm_apply_coe, ofConjAct_toConjAct, ofConjAct_mul, ofConjAct_inv, to_mul_symm_eq, Equiv.Perm.mem_conj_support, toConjAct_ofConjAct, ofConjAct_one, smul_eq_mulAut_conj
rec 📖	CompOp	—
toConjAct 📖	CompOp	36 math math: toConjAct_inv, toConjAct_mul, stabilizer_eq_centralizer, CongruenceSubgroup.exists_Gamma_le_conj', CongruenceSubgroup.conjGL_coe, forall, IsCusp.of_isFiniteRelIndex_conj, toConjAct_zero, SlashInvariantForm.coe_translate, Subgroup.conjAct_pointwise_smul_iff, lipschitzGroup.conjAct_smul_ι_mem_range_ι, spinGroup.units_involute_act_eq_conjAct, Subgroup.Commensurable.commensurator_mem_iff, spinGroup.conjAct_smul_ι_mem_range_ι, spinGroup.conjAct_smul_range_ι, CongruenceSubgroup.IsArithmetic.conj, CongruenceSubgroup.isArithmetic_conj_SL2Z, of_mul_symm_eq, pinGroup.conjAct_smul_ι_mem_range_ι, CuspForm.coe_translate, Unitary.toAlgEquiv_conjStarAlgAut, toConjAct_smul, pinGroup.conjAct_smul_range_ι, Unitary.toRingEquiv_conjStarAlgAut, ofConjAct_toConjAct, Equiv.Perm.OnCycleFactors.Subgroup.Centralizer.toConjAct_smul_mem_cycleFactorsFinset, Subgroup.conjAct_pointwise_smul_eq_self, Equiv.Perm.cycleFactorsFinset_conj, to_mul_symm_eq, ModularForm.coe_translate, toConjAct_ofConjAct, toConjAct_one, Subgroup.IsArithmetic.conj, lipschitzGroup.conjAct_smul_range_ι, IsCusp.smul, Subgroup.centralizer_eq_comap_stabilizer
unitsMulDistribMulAction 📖	CompOp	—
unitsScalar 📖	CompOp	8 math math: unitsSMulCommClass', unitsSMulCommClass, lipschitzGroup.conjAct_smul_ι_mem_range_ι, spinGroup.units_involute_act_eq_conjAct, spinGroup.conjAct_smul_ι_mem_range_ι, units_smul_def, pinGroup.conjAct_smul_ι_mem_range_ι, units_continuousConstSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card 📖	mathematical	—	Fintype.card ConjAct instFintype	—	—
fixedPoints_eq_center 📖	mathematical	—	MulAction.fixedPoints ConjAct DivInvMonoid.toMonoid instDivInvMonoid Group.toDivInvMonoid MulDistribMulAction.toMulAction instMulDistribMulAction SetLike.coe Subgroup Subgroup.instSetLike Subgroup.center	—	Set.ext
forall 📖	mathematical	—	DFunLike.coe MulEquiv ConjAct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid instDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike toConjAct	—	—
mem_orbit_conjAct 📖	mathematical	—	Set Set.instMembership MulAction.orbit ConjAct instSMul Group.toDivInvMonoid IsConj DivInvMonoid.toMonoid	—	isConj_comm isConj_iff MulAction.mem_orbit_iff
normal_of_characteristic_of_normal 📖	mathematical	—	Subgroup.Normal Subgroup.map Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Subgroup.subtype	—	Subgroup.apply_coe_mem_map SetLike.ext_iff Subgroup.Characteristic.fixed
ofConjAct_inv 📖	mathematical	—	DFunLike.coe MulEquiv ConjAct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid instDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike ofConjAct DivInvMonoid.toInv	—	—
ofConjAct_mul 📖	mathematical	—	DFunLike.coe MulEquiv ConjAct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid instDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike ofConjAct	—	—
ofConjAct_one 📖	mathematical	—	DFunLike.coe MulEquiv ConjAct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid instDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike ofConjAct MulOne.toOne	—	—
ofConjAct_toConjAct 📖	mathematical	—	DFunLike.coe MulEquiv ConjAct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid instDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike ofConjAct toConjAct	—	—
of_mul_symm_eq 📖	mathematical	—	MulEquiv.symm ConjAct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid instDivInvMonoid ofConjAct toConjAct	—	—
orbitRel_conjAct 📖	mathematical	—	MulAction.orbitRel ConjAct instGroup MulDistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid instMulDistribMulAction IsConj	—	MulAction.orbitRel_apply mem_orbit_conjAct
orbit_eq_carrier_conjClasses 📖	mathematical	—	MulAction.orbit ConjAct instSMul Group.toDivInvMonoid ConjClasses.carrier DivInvMonoid.toMonoid	—	Set.ext ConjClasses.mem_carrier_iff_mk_eq ConjClasses.mk_eq_mk_iff_isConj mem_orbit_conjAct
smulCommClass 📖	mathematical	—	SMulCommClass ConjAct instSMul Group.toDivInvMonoid	—	smul_def mul_smul_comm smul_mul_assoc
smulCommClass' 📖	mathematical	—	SMulCommClass ConjAct instSMul Group.toDivInvMonoid	—	SMulCommClass.symm smulCommClass
smul_def 📖	mathematical	—	ConjAct instSMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid DFunLike.coe MulEquiv instDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike ofConjAct DivInvMonoid.toInv	—	—
smul_eq_mulAut_conj 📖	mathematical	—	ConjAct instSMul Group.toDivInvMonoid DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid EquivLike.toFunLike MulEquiv.instEquivLike MonoidHom MulAut MulAut.instGroup MonoidHom.instFunLike MulAut.conj instDivInvMonoid ofConjAct	—	—
stabilizer_eq_centralizer 📖	mathematical	—	MulAction.stabilizer ConjAct instGroup MulDistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid instMulDistribMulAction Subgroup.centralizer Set Set.instSingletonSet DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike toConjAct	—	le_antisymm eq_mul_inv_iff_mul_eq mul_inv_eq_of_eq_mul
toConjAct_inv 📖	mathematical	—	DFunLike.coe MulEquiv ConjAct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid instDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike toConjAct DivInvMonoid.toInv	—	—
toConjAct_mul 📖	mathematical	—	DFunLike.coe MulEquiv ConjAct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid instDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike toConjAct	—	—
toConjAct_ofConjAct 📖	mathematical	—	DFunLike.coe MulEquiv ConjAct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid instDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike toConjAct ofConjAct	—	—
toConjAct_one 📖	mathematical	—	DFunLike.coe MulEquiv ConjAct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid instDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike toConjAct MulOne.toOne	—	—
toConjAct_smul 📖	mathematical	—	ConjAct instSMul DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid instDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike toConjAct DivInvMonoid.toInv	—	—
to_mul_symm_eq 📖	mathematical	—	MulEquiv.symm ConjAct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid instDivInvMonoid toConjAct ofConjAct	—	—
unitsSMulCommClass 📖	mathematical	—	SMulCommClass ConjAct Units unitsScalar	—	units_smul_def mul_smul_comm smul_mul_assoc
unitsSMulCommClass' 📖	mathematical	—	SMulCommClass ConjAct Units unitsScalar	—	SMulCommClass.symm unitsSMulCommClass
units_smul_def 📖	mathematical	—	ConjAct Units unitsScalar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Units.val DFunLike.coe MulEquiv DivInvMonoid.toMonoid instDivInvMonoid Units.instDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike ofConjAct Units.instInv	—	—

ConjAct.Subgroup

Definitions

Name	Category	Theorems
conjAction 📖	CompOp	1 math math: val_conj_smul
conjMulDistribMulAction 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
val_conj_smul 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike ConjAct conjAction ConjAct.instSMul Group.toDivInvMonoid	—	—

MulAut

Definitions

Name	Category	Theorems
conjNormal 📖	CompOp	4 math math: conjNormal_symm_apply, conjNormal_val, conjNormal_inv_apply, conjNormal_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjNormal_apply 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike DFunLike.coe MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MonoidHom MulAut MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike conjNormal MulOne.toMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
conjNormal_inv_apply 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike DFunLike.coe MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulAut InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid instGroup MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike conjNormal MulOne.toMul	—	conjNormal_symm_apply
conjNormal_symm_apply 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike DFunLike.coe MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm MonoidHom MulAut MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike conjNormal MulOne.toMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	inv_inv
conjNormal_val 📖	mathematical	—	DFunLike.coe MonoidHom MulAut Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.mul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike conjNormal MulOne.toMul Subgroup.toGroup conj	—	MulEquiv.ext

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
centralizer_eq_comap_stabilizer 📖	mathematical	—	centralizer Set Set.instSingletonSet comap ConjAct.instGroup ConjAct MulEquiv.toMonoidHom Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid ConjAct.instDivInvMonoid ConjAct.toConjAct MulAction.stabilizer MulDistribMulAction.toMulAction ConjAct.instMulDistribMulAction	—	ext mul_inv_eq_iff_eq_mul

(root)

Definitions

Name	Category	Theorems
unitsCentralizerEquiv 📖	CompOp	2 math math: val_unitsCentralizerEquiv_apply_coe, val_unitsCentralizerEquiv_symm_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
val_unitsCentralizerEquiv_apply_coe 📖	mathematical	—	Units.val ConjAct Units Subgroup ConjAct.instGroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer MulDistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid ConjAct.instMulDistribMulAction DFunLike.coe MulEquiv Submonoid Monoid.toMulOneClass Submonoid.instSetLike Submonoid.centralizer Set Set.instSingletonSet Submonoid.toMonoid Units.instMul Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike unitsCentralizerEquiv	—	—
val_unitsCentralizerEquiv_symm_apply_coe 📖	mathematical	—	Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.centralizer Set Set.instSingletonSet Units.val Submonoid.toMonoid DFunLike.coe MulEquiv ConjAct Units Subgroup ConjAct.instGroup Units.instGroup Subgroup.instSetLike MulAction.stabilizer MulDistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid ConjAct.instMulDistribMulAction Subgroup.mul Units.instMul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm unitsCentralizerEquiv MulOne.toMul MulOneClass.toMulOne ConjAct.instDivInvMonoid Units.instDivInvMonoid ConjAct.ofConjAct	—	—

---

← Back to Index