Documentation Verification Report

Quotient

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

Statistics

Metric	Count
Definitions `QuotientAction`, `addLeftCosetsCompSubtypeVal`, `equivAddSubgroupOrbits`, `equivAddSubgroupOrbitsQuotientAddGroup`, `equivAddSubgroupOrbitsSetoidComap`, `ofQuotientStabilizer`, `orbitEquivQuotientStabilizer`, `orbitProdStabilizerEquivAddGroup`, `quotient`, `selfEquivOrbitsQuotientProd`, `selfEquivOrbitsQuotientProd'`, `selfEquivSigmaOrbitsQuotientStabilizer`, `selfEquivSigmaOrbitsQuotientStabilizer'`, `sigmaFixedByEquivOrbitsProdAddGroup`, `QuotientAction`, `equivSubgroupOrbits`, `equivSubgroupOrbitsQuotientGroup`, `equivSubgroupOrbitsSetoidComap`, `mulLeftCosetsCompSubtypeVal`, `ofQuotientStabilizer`, `orbitEquivQuotientStabilizer`, `orbitProdStabilizerEquivGroup`, `quotient`, `selfEquivOrbitsQuotientProd`, `selfEquivOrbitsQuotientProd'`, `selfEquivSigmaOrbitsQuotientStabilizer`, `selfEquivSigmaOrbitsQuotientStabilizer'`, `sigmaFixedByEquivOrbitsProdGroup`, `toQuotient`, `quotientCenterEmbedding`, `quotientCentralizerEmbedding`	31
Theorems `coe_vadd_out`, `mk_vadd_out`, `vadd_coe`, `vadd_mk`, `inv_mul_mem`, `card_orbit_mul_card_stabilizer_eq_card_addGroup`, `finite_quotient_of_finite_quotient_of_finite_quotient`, `finite_quotient_of_pretransitive_of_finite_quotient`, `injective_ofQuotientStabilizer`, `isPretransitive_quotient`, `left_quotientAction`, `ofQuotientStabilizer_mem_orbit`, `ofQuotientStabilizer_mk`, `ofQuotientStabilizer_vadd`, `orbitEquivQuotientStabilizer_symm_apply`, `right_quotientAction`, `right_quotientAction'`, `stabilizer_quotient`, `sum_card_fixedBy_eq_card_orbits_mul_card_addGroup`, `card_carrier`, `coe_smul_out`, `mk_smul_out`, `smul_coe`, `smul_mk`, `inv_mul_mem`, `card_orbit_mul_card_stabilizer_eq_card_group`, `finite_quotient_of_finite_quotient_of_finite_quotient`, `finite_quotient_of_pretransitive_of_finite_quotient`, `injective_ofQuotientStabilizer`, `isPretransitive_quotient`, `left_quotientAction`, `ofQuotientStabilizer_mem_orbit`, `ofQuotientStabilizer_mk`, `ofQuotientStabilizer_smul`, `orbitEquivQuotientStabilizer_symm_apply`, `right_quotientAction`, `right_quotientAction'`, `stabilizer_quotient`, `sum_card_fixedBy_eq_card_orbits_mul_card_group`, `toQuotient_apply`, `out_conj_pow_minimalPeriod_mem`, `normalCore_eq_ker`, `quotientCenterEmbedding_apply`, `quotientCentralizerEmbedding_apply`	44
Total	75

AddAction

Definitions

Name	Category	Theorems
`QuotientAction` 📖	CompData	3 math math: `left_quotientAction`, `right_quotientAction`, `right_quotientAction'`
`addLeftCosetsCompSubtypeVal` 📖	CompOp	—
`equivAddSubgroupOrbits` 📖	CompOp	—
`equivAddSubgroupOrbitsQuotientAddGroup` 📖	CompOp	—
`equivAddSubgroupOrbitsSetoidComap` 📖	CompOp	—
`ofQuotientStabilizer` 📖	CompOp	4 math math: `injective_ofQuotientStabilizer`, `ofQuotientStabilizer_mem_orbit`, `ofQuotientStabilizer_vadd`, `ofQuotientStabilizer_mk`
`orbitEquivQuotientStabilizer` 📖	CompOp	1 math math: `orbitEquivQuotientStabilizer_symm_apply`
`orbitProdStabilizerEquivAddGroup` 📖	CompOp	—
`quotient` 📖	CompOp	13 math math: `QuotientAddGroup.measurableVAdd`, `Quotient.vadd_coe`, `Quotient.coe_vadd_out`, `QuotientAddGroup.instContinuousVAdd`, `Quotient.mk_vadd_out`, `AddSubgroup.vadd_leftQuotientEquiv`, `QuotientAddGroup.instContinuousConstVAdd`, `Quotient.vadd_mk`, `AddSubgroup.vadd_apply_eq_vadd_apply_neg_vadd`, `MeasureTheory.AddQuotientMeasureEqMeasurePreimage.vaddInvariantMeasure_quotient`, `ofQuotientStabilizer_vadd`, `isPretransitive_quotient`, `stabilizer_quotient`
`selfEquivOrbitsQuotientProd` 📖	CompOp	—
`selfEquivOrbitsQuotientProd'` 📖	CompOp	—
`selfEquivSigmaOrbitsQuotientStabilizer` 📖	CompOp	—
`selfEquivSigmaOrbitsQuotientStabilizer'` 📖	CompOp	—
`sigmaFixedByEquivOrbitsProdAddGroup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_orbit_mul_card_stabilizer_eq_card_addGroup` 📖	mathematical	—	`Fintype.card` `Set.Elem` `orbit` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `stabilizer`	—	`Fintype.card_prod` `Fintype.card_congr`
`finite_quotient_of_finite_quotient_of_finite_quotient` 📖	mathematical	—	`Finite` `orbitRel.Quotient` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.toAddGroup` `instAddAction`	—	`Equiv.finite_iff` `Finite.instSigma` `finite_quotient_of_pretransitive_of_finite_quotient` `instIsPretransitiveElemOrbit_1`
`finite_quotient_of_pretransitive_of_finite_quotient` 📖	mathematical	—	`Finite` `orbitRel.Quotient` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.toAddGroup` `instAddAction`	—	`isEmpty_or_nonempty` `Quotient.finite` `Finite.of_subsingleton` `IsEmpty.instSubsingleton` `Finite.of_equiv` `Setoid.symm'` `Quotient.eq` `orbitRel_apply` `mem_orbit_iff` `QuotientAddGroup.rightRel_eq` `AddSemigroupAction.add_vadd` `neg_vadd_vadd` `Finite.of_surjective` `Quotient.surjective_liftOn'` `Quotient.mk''_surjective` `surjective_vadd`
`injective_ofQuotientStabilizer` 📖	mathematical	—	`HasQuotient.Quotient` `AddSubgroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `stabilizer` `ofQuotientStabilizer`	—	`Quotient.inductionOn₂'` `Quotient.sound'` `QuotientAddGroup.leftRel_apply` `AddSemigroupAction.add_vadd` `neg_vadd_vadd`
`isPretransitive_quotient` 📖	mathematical	—	`IsPretransitive` `HasQuotient.Quotient` `AddSubgroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `quotient` `AddMonoid.toAddAction` `left_quotientAction`	—	`left_quotientAction` `QuotientAddGroup.eq` `neg_add_cancel_right` `neg_add_cancel` `AddSubgroup.zero_mem`
`left_quotientAction` 📖	mathematical	—	`QuotientAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoid.toAddAction`	—	`vadd_eq_add` `neg_add_rev` `add_assoc` `neg_add_cancel_left`
`ofQuotientStabilizer_mem_orbit` 📖	mathematical	—	`Set` `Set.instMembership` `orbit` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `ofQuotientStabilizer`	—	`Quotient.inductionOn'`
`ofQuotientStabilizer_mk` 📖	mathematical	—	`ofQuotientStabilizer` `stabilizer` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction`	—	—
`ofQuotientStabilizer_vadd` 📖	mathematical	—	`ofQuotientStabilizer` `HVAdd.hVAdd` `HasQuotient.Quotient` `AddSubgroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `stabilizer` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `quotient` `AddMonoid.toAddAction` `left_quotientAction`	—	`Quotient.inductionOn'` `left_quotientAction` `AddSemigroupAction.add_vadd`
`orbitEquivQuotientStabilizer_symm_apply` 📖	mathematical	—	`Set` `Set.instMembership` `orbit` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `DFunLike.coe` `Equiv` `HasQuotient.Quotient` `AddSubgroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `stabilizer` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `orbitEquivQuotientStabilizer` `HVAdd.hVAdd` `instHVAdd`	—	—
`right_quotientAction` 📖	mathematical	—	`QuotientAction` `AddOpposite` `AddSubgroup` `AddOpposite.instAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.op` `AddSubgroup.normalizer` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `instAddAction` `AddMonoid.toOppositeAddAction`	—	`AddSubgroup.vadd_def` `AddOpposite.vadd_eq_add_unop` `neg_add_rev` `add_assoc` `AddSubgroup.mem_normalizer_iff'` `Subtype.prop` `add_neg_cancel_left`
`right_quotientAction'` 📖	mathematical	—	`QuotientAction` `AddOpposite` `AddOpposite.instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoid.toOppositeAddAction`	—	`AddOpposite.vadd_eq_add_unop` `neg_add_rev` `add_assoc` `AddSubgroup.Normal.mem_comm_iff` `add_neg_cancel_right`
`stabilizer_quotient` 📖	mathematical	—	`stabilizer` `HasQuotient.Quotient` `AddSubgroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `quotient` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoid.toAddAction` `left_quotientAction` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`AddSubgroup.ext` `left_quotientAction` `mem_stabilizer_iff` `add_zero` `QuotientAddGroup.eq` `neg_mem_iff` `AddSubgroupClass.toNegMemClass` `AddSubgroup.instAddSubgroupClass`
`sum_card_fixedBy_eq_card_orbits_mul_card_addGroup` 📖	mathematical	—	`Finset.sum` `Nat.instAddCommMonoid` `Finset.univ` `Fintype.card` `Set.Elem` `fixedBy` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `orbitRel`	—	`Fintype.card_prod` `Fintype.card_sigma` `Fintype.card_congr`

AddAction.Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_vadd_out` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `Quotient.out` `QuotientAddGroup.leftRel` `HasQuotient.Quotient` `AddSubgroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `AddAction.quotient`	—	`mk_vadd_out`
`mk_vadd_out` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `Quotient.out` `QuotientAddGroup.leftRel` `HasQuotient.Quotient` `AddSubgroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `AddAction.quotient`	—	`QuotientAddGroup.out_eq'`
`vadd_coe` 📖	mathematical	—	`HVAdd.hVAdd` `HasQuotient.Quotient` `AddSubgroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddAction.quotient`	—	—
`vadd_mk` 📖	mathematical	—	`HVAdd.hVAdd` `HasQuotient.Quotient` `AddSubgroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddAction.quotient`	—	—

AddAction.QuotientAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inv_mul_mem` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddAction.toAddSemigroupAction`	—	—

ConjClasses

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_carrier` 📖	mathematical	—	`Fintype.card` `Set.Elem` `carrier` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `ConjAct` `Subgroup` `ConjAct.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `MulDistribMulAction.toMulAction` `ConjAct.instMulDistribMulAction`	—	`Fintype.card_congr` `MulAction.card_orbit_mul_card_stabilizer_eq_card_group` `Fintype.card_pos_iff` `One.instNonempty` `Fintype.card_congr'` `ConjAct.orbit_eq_carrier_conjClasses`

MulAction

Definitions

Name	Category	Theorems
`QuotientAction` 📖	CompData	3 math math: `right_quotientAction'`, `right_quotientAction`, `left_quotientAction`
`equivSubgroupOrbits` 📖	CompOp	—
`equivSubgroupOrbitsQuotientGroup` 📖	CompOp	—
`equivSubgroupOrbitsSetoidComap` 📖	CompOp	—
`mulLeftCosetsCompSubtypeVal` 📖	CompOp	7 math math: `Subgroup.quotientEquivSigmaZMod_apply`, `Subgroup.transferTransversal_apply'`, `Subgroup.transferFunction_apply`, `Subgroup.transferTransversal_apply''`, `Subgroup.quotientEquivSigmaZMod_symm_apply`, `MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot`, `Sylow.mem_fixedPoints_mul_left_cosets_iff_mem_normalizer`
`ofQuotientStabilizer` 📖	CompOp	4 math math: `ofQuotientStabilizer_mem_orbit`, `ofQuotientStabilizer_mk`, `injective_ofQuotientStabilizer`, `ofQuotientStabilizer_smul`
`orbitEquivQuotientStabilizer` 📖	CompOp	1 math math: `orbitEquivQuotientStabilizer_symm_apply`
`orbitProdStabilizerEquivGroup` 📖	CompOp	—
`quotient` 📖	CompOp	29 math math: `Quotient.coe_smul_out`, `Quotient.smul_mk`, `Subgroup.smul_leftQuotientEquiv`, `Subgroup.smul_apply_eq_smul_apply_inv_smul`, `Action.FintypeCat.toEndHom_apply`, `isPretransitive_quotient`, `QuotientGroup.measurableSMul`, `MeasureTheory.QuotientMeasureEqMeasurePreimage.smulInvariantMeasure_quotient`, `Subgroup.quotientEquivSigmaZMod_apply`, `Action.FintypeCat.quotientToEndHom_mk`, `stabilizer_quotient`, `Quotient.mk_smul_out`, `Subgroup.transferTransversal_apply'`, `QuotientGroup.instContinuousSMul`, `MulActionHom.toQuotient_apply`, `CategoryTheory.PreGaloisCategory.has_decomp_quotients`, `Action.FintypeCat.quotientToQuotientOfLE_hom_mk`, `Subgroup.normalCore_eq_ker`, `QuotientGroup.instContinuousConstSMul`, `Subgroup.transferFunction_apply`, `Subgroup.transferTransversal_apply''`, `Subgroup.quotientEquivSigmaZMod_symm_apply`, `CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroup`, `MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot`, `ofQuotientStabilizer_smul`, `Quotient.smul_coe`, `Action.FintypeCat.toEndHom_trivial_of_mem`, `QuotientGroup.out_conj_pow_minimalPeriod_mem`, `AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero`
`selfEquivOrbitsQuotientProd` 📖	CompOp	—
`selfEquivOrbitsQuotientProd'` 📖	CompOp	—
`selfEquivSigmaOrbitsQuotientStabilizer` 📖	CompOp	—
`selfEquivSigmaOrbitsQuotientStabilizer'` 📖	CompOp	—
`sigmaFixedByEquivOrbitsProdGroup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_orbit_mul_card_stabilizer_eq_card_group` 📖	mathematical	—	`Fintype.card` `Set.Elem` `orbit` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `stabilizer`	—	`Fintype.card_prod` `Fintype.card_congr`
`finite_quotient_of_finite_quotient_of_finite_quotient` 📖	mathematical	—	`Finite` `orbitRel.Quotient` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `instMulAction`	—	`Equiv.finite_iff` `Finite.instSigma` `finite_quotient_of_pretransitive_of_finite_quotient` `instIsPretransitiveElemOrbit_1`
`finite_quotient_of_pretransitive_of_finite_quotient` 📖	mathematical	—	`Finite` `orbitRel.Quotient` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `instMulAction`	—	`isEmpty_or_nonempty` `Quotient.finite` `Finite.of_subsingleton` `IsEmpty.instSubsingleton` `Finite.of_equiv` `Setoid.symm'` `QuotientGroup.rightRel_eq` `SemigroupAction.mul_smul` `inv_smul_smul` `Finite.of_surjective` `Quotient.surjective_liftOn'` `Quotient.mk''_surjective` `surjective_smul`
`injective_ofQuotientStabilizer` 📖	mathematical	—	`HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `stabilizer` `ofQuotientStabilizer`	—	`Quotient.inductionOn₂'` `Quotient.sound'` `QuotientGroup.leftRel_apply` `SemigroupAction.mul_smul` `inv_smul_smul`
`isPretransitive_quotient` 📖	mathematical	—	`IsPretransitive` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `quotient` `Monoid.toMulAction` `left_quotientAction`	—	`left_quotientAction` `QuotientGroup.eq` `inv_mul_cancel_right` `inv_mul_cancel` `Subgroup.one_mem`
`left_quotientAction` 📖	mathematical	—	`QuotientAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Monoid.toMulAction`	—	`smul_eq_mul` `mul_inv_rev` `mul_assoc` `inv_mul_cancel_left`
`ofQuotientStabilizer_mem_orbit` 📖	mathematical	—	`Set` `Set.instMembership` `orbit` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `ofQuotientStabilizer`	—	`Quotient.inductionOn'`
`ofQuotientStabilizer_mk` 📖	mathematical	—	`ofQuotientStabilizer` `stabilizer` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction`	—	—
`ofQuotientStabilizer_smul` 📖	mathematical	—	`ofQuotientStabilizer` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `stabilizer` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `quotient` `Monoid.toMulAction` `left_quotientAction`	—	`Quotient.inductionOn'` `left_quotientAction` `SemigroupAction.mul_smul`
`orbitEquivQuotientStabilizer_symm_apply` 📖	mathematical	—	`Set` `Set.instMembership` `orbit` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `DFunLike.coe` `Equiv` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `stabilizer` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `orbitEquivQuotientStabilizer`	—	—
`right_quotientAction` 📖	mathematical	—	`QuotientAction` `MulOpposite` `Subgroup` `MulOpposite.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.op` `Subgroup.normalizer` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `instMulAction` `Monoid.toOppositeMulAction`	—	`Subgroup.smul_def` `MulOpposite.smul_eq_mul_unop` `mul_inv_rev` `mul_assoc` `Subgroup.mem_normalizer_iff'` `Subtype.prop` `mul_inv_cancel_left`
`right_quotientAction'` 📖	mathematical	—	`QuotientAction` `MulOpposite` `MulOpposite.instMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Monoid.toOppositeMulAction`	—	`MulOpposite.smul_eq_mul_unop` `mul_inv_rev` `mul_assoc` `Subgroup.Normal.mem_comm_iff` `mul_inv_cancel_right`
`stabilizer_quotient` 📖	mathematical	—	`stabilizer` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `quotient` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Monoid.toMulAction` `left_quotientAction` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Subgroup.ext` `left_quotientAction` `mul_one` `SubgroupClass.toInvMemClass` `Subgroup.instSubgroupClass`
`sum_card_fixedBy_eq_card_orbits_mul_card_group` 📖	mathematical	—	`Finset.sum` `Nat.instAddCommMonoid` `Finset.univ` `Fintype.card` `Set.Elem` `fixedBy` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `orbitRel`	—	`Fintype.card_prod` `Fintype.card_sigma` `Fintype.card_congr`

MulAction.Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_smul_out` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Quotient.out` `QuotientGroup.leftRel` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `MulAction.quotient`	—	`mk_smul_out`
`mk_smul_out` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Quotient.out` `QuotientGroup.leftRel` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `MulAction.quotient`	—	`QuotientGroup.out_eq'`
`smul_coe` 📖	mathematical	—	`HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulAction.quotient`	—	—
`smul_mk` 📖	mathematical	—	`HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulAction.quotient`	—	—

MulAction.QuotientAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inv_mul_mem` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	—

MulActionHom

Definitions

Name	Category	Theorems
`toQuotient` 📖	CompOp	1 math math: `toQuotient_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toQuotient_apply` 📖	mathematical	—	`DFunLike.coe` `MulActionHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `MulAction.quotient` `MulAction.left_quotientAction` `instFunLikeMulActionHom` `toQuotient`	—	`MulAction.left_quotientAction`

QuotientGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`out_conj_pow_minimalPeriod_mem` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Quotient.out` `leftRel` `Monoid.toNatPow` `Function.minimalPeriod` `HasQuotient.Quotient` `instHasQuotientSubgroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulAction.quotient` `Monoid.toMulAction` `MulAction.left_quotientAction`	—	`MulAction.left_quotientAction` `mul_assoc` `eq` `out_eq'` `smul_eq_mul` `MulAction.Quotient.mk_smul_out` `MulAction.pow_smul_eq_iff_minimalPeriod_dvd` `dvd_refl`

Subgroup

Definitions

Name	Category	Theorems
`quotientCenterEmbedding` 📖	CompOp	1 math math: `quotientCenterEmbedding_apply`
`quotientCentralizerEmbedding` 📖	CompOp	1 math math: `quotientCentralizerEmbedding_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`normalCore_eq_ker` 📖	mathematical	—	`normalCore` `MonoidHom.ker` `Equiv.Perm` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `MulAction.toPermHom` `MulAction.quotient` `Monoid.toMulAction` `MulAction.left_quotientAction`	—	`le_antisymm` `MulAction.left_quotientAction` `Equiv.Perm.ext` `QuotientGroup.induction_on` `QuotientGroup.eq` `smul_eq_mul` `mul_inv_rev` `inv_inv` `inv_mem` `normal_le_normalCore` `MonoidHom.normal_ker` `inv_mem_iff` `mul_one` `Equiv.Perm.ext_iff`
`quotientCenterEmbedding_apply` 📖	mathematical	`closure` `Top.top` `Subgroup` `instTop`	`DFunLike.coe` `Function.Embedding` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup` `center` `Function.instFunLikeEmbedding` `quotientCenterEmbedding` `Set` `Set.instMembership` `commutatorSet` `Bracket.bracket` `commutatorElement`	—	—
`quotientCentralizerEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `centralizer` `Set` `Set.instSingletonSet` `Set.Elem` `commutatorSet` `Function.instFunLikeEmbedding` `quotientCentralizerEmbedding` `Set.instMembership` `Bracket.bracket` `commutatorElement`	—	—

---

← Back to Index