OfQuotient

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

Statistics

Metric	Count
Definitions instQuotientSubgroupElemFixedPointsSubtypeMem, instQuotientSubgroupSubtypeMemSubgroup, instQuotientSubgroupSubtypeMemSubmonoidSubmonoid	3
Theorems coe_quotient_smul_fixedPoints, quotient_out_smul_fixedPoints	2
Total	5

MulAction

Definitions

Name	Category	Theorems
instQuotientSubgroupElemFixedPointsSubtypeMem 📖	CompOp	2 math math: quotient_out_smul_fixedPoints, coe_quotient_smul_fixedPoints

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_quotient_smul_fixedPoints 📖	mathematical	—	HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup Set.Elem fixedPoints SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup instMulAction SemigroupAction.toSMul Monoid.toSemigroup QuotientGroup.Quotient.group toSemigroupAction instQuotientSubgroupElemFixedPointsSubtypeMem instMulActionElemFixedPointsSubtypeMemSubgroupOfNormal	—	—
quotient_out_smul_fixedPoints 📖	mathematical	—	Set.Elem fixedPoints Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup instMulAction SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction instMulActionElemFixedPointsSubtypeMemSubgroupOfNormal Quotient.out QuotientGroup.leftRel HasQuotient.Quotient QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group instQuotientSubgroupElemFixedPointsSubtypeMem	—	Quotient.out_eq

MulDistribMulAction

Definitions

Name	Category	Theorems
instQuotientSubgroupSubtypeMemSubgroup 📖	CompOp	—
instQuotientSubgroupSubtypeMemSubmonoidSubmonoid 📖	CompOp	—

---

← Back to Index