Documentation Verification Report

ConjAct

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

Statistics

Metric	Count
Definitions `ConjAct`	1
Theorems `cycleFactorsFinset_conj`, `cycleFactorsFinset_conj_eq`, `mem_conj_support`, `mem_cycleFactorsFinset_conj'`	4
Total	5

Equiv.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cycleFactorsFinset_conj` 📖	mathematical	—	`cycleFactorsFinset` `ConjAct` `Equiv.Perm` `ConjAct.instSMul` `Group.toDivInvMonoid` `permGroup` `DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `ConjAct.instDivInvMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `ConjAct.toConjAct` `Finset.map` `Equiv.toEmbedding` `MulEquiv.toEquiv` `MonoidHom` `MulAut` `MulAut.instGroup` `MonoidHom.instFunLike` `MulAut.conj`	—	`Finset.ext` `ConjAct.smul_def` `ConjAct.ofConjAct_toConjAct` `Finset.mem_map_equiv` `mem_cycleFactorsFinset_conj` `mul_assoc` `mul_inv_cancel_left` `mul_inv_cancel` `mul_one`
`cycleFactorsFinset_conj_eq` 📖	mathematical	—	`cycleFactorsFinset` `ConjAct` `Equiv.Perm` `ConjAct.instSMul` `Group.toDivInvMonoid` `permGroup` `Finset` `Finset.smulFinset` `Fintype.decidableEqEquivFintype`	—	`Finset.ext` `mem_cycleFactorsFinset_conj'` `inv_smul_smul` `Finset.inv_smul_mem_iff`
`mem_conj_support` 📖	mathematical	—	`Finset` `Finset.instMembership` `support` `ConjAct` `Equiv.Perm` `ConjAct.instSMul` `Group.toDivInvMonoid` `permGroup` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `ConjAct.instDivInvMonoid` `MulEquiv.instEquivLike` `ConjAct.ofConjAct` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `ConjAct.instGroup`	—	`Equiv.apply_eq_iff_eq_symm_apply`
`mem_cycleFactorsFinset_conj'` 📖	mathematical	—	`Equiv.Perm` `Finset` `Finset.instMembership` `cycleFactorsFinset` `ConjAct` `ConjAct.instSMul` `Group.toDivInvMonoid` `permGroup`	—	`mem_cycleFactorsFinset_conj`

(root)

Definitions

Name	Category	Theorems
`ConjAct` 📖	CompOp	72 math math: `ConjAct.smul_def`, `ConjAct.fixedPoints_eq_center`, `ConjAct.toConjAct_inv`, `ConjAct.toConjAct_mul`, `ConjAct.stabilizer_eq_centralizer`, `CongruenceSubgroup.exists_Gamma_le_conj'`, `CongruenceSubgroup.conjGL_coe`, `ConjAct.unitsSMulCommClass'`, `ConjAct.unitsSMulCommClass`, `ConjAct.forall`, `val_unitsCentralizerEquiv_apply_coe`, `IsCusp.of_isFiniteRelIndex_conj`, `ConjAct.toConjAct_zero`, `ConjAct.smulCommClass₀`, `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`, `ConjAct.smulCommClass₀'`, `spinGroup.conjAct_smul_ι_mem_range_ι`, `ConjAct.smulCommClass'`, `spinGroup.conjAct_smul_range_ι`, `ConjAct.ofConjAct_zero`, `CongruenceSubgroup.IsArithmetic.conj`, `CongruenceSubgroup.Gamma_cong_eq_self`, `ConjAct.units_smul_def`, `Subgroup.normalCore_eq_iInf_conjAct`, `CongruenceSubgroup.isArithmetic_conj_SL2Z`, `ConjAct.card`, `ConjAct.of_mul_symm_eq`, `pinGroup.conjAct_smul_ι_mem_range_ι`, `CuspForm.coe_translate`, `Unitary.toAlgEquiv_conjStarAlgAut`, `ConjAct.smulCommClass`, `ConjAct.toConjAct_smul`, `pinGroup.conjAct_smul_range_ι`, `val_unitsCentralizerEquiv_symm_apply_coe`, `Subgroup.Commensurable.commensurable_inv`, `Equiv.Perm.mem_cycleFactorsFinset_conj'`, `Unitary.toRingEquiv_conjStarAlgAut`, `Subgroup.Commensurable.conj`, `ConjAct.units_continuousConstSMul`, `ConjAct.ofConjAct_toConjAct`, `Equiv.Perm.OnCycleFactors.Subgroup.Centralizer.toConjAct_smul_mem_cycleFactorsFinset`, `ConjAct.Subgroup.val_conj_smul`, `Equiv.Perm.cycleFactorsFinset_conj_eq`, `Subgroup.conjAct_pointwise_smul_eq_self`, `ConjAct.mem_orbit_conjAct`, `Subgroup.Commensurable.commensurator'_mem_iff`, `Equiv.Perm.cycleFactorsFinset_conj`, `ConjAct.orbit_eq_carrier_conjClasses`, `CongruenceSubgroup.conj_cong_is_cong`, `Module.End.mulSemiringActionToAlgEquiv_conjAct_surjective`, `ConjAct.ofConjAct_mul`, `ConjAct.orbitRel_conjAct`, `ConjAct.ofConjAct_inv`, `ConjAct.to_mul_symm_eq`, `ModularForm.coe_translate`, `Equiv.Perm.mem_conj_support`, `ConjClasses.card_carrier`, `ConjAct.toConjAct_ofConjAct`, `ConjAct.toConjAct_one`, `Subgroup.nat_card_centralizer_nat_card_stabilizer`, `ConjAct.ofConjAct_one`, `Subgroup.IsArithmetic.conj`, `lipschitzGroup.conjAct_smul_range_ι`, `IsCusp.smul`, `ConjAct.smul_eq_mulAut_conj`, `Subgroup.centralizer_eq_comap_stabilizer`

---

← Back to Index