Basic

📁 Source: Mathlib/GroupTheory/Coset/Basic.lean

Statistics

Metric	Count
Definitions `fiberEquiv`, `fiberEquivKer`, `fiberEquivKerOfSurjective`, `fiberEquivOfSurjective`, `addGroupEquivQuotientProdAddSubgroup`, `leftCosetEquivAddSubgroup`, `quotientAddSubgroupOfEmbeddingOfLE`, `quotientAddSubgroupOfMapOfLE`, `quotientEquivProdOfLE`, `quotientEquivProdOfLE'`, `quotientMapOfLE`, `quotientiInfAddSubgroupOfEmbedding`, `quotientiInfEmbedding`, `rightCosetEquivAddSubgroup`, `LeftAddCosetEquivalence`, `LeftCosetEquivalence`, `fiberEquiv`, `fiberEquivKer`, `fiberEquivKerOfSurjective`, `fiberEquivOfSurjective`, `preimageMkEquivAddSubgroupProdSet`, `quotientEquivSelf`, `preimageMkEquivSubgroupProdSet`, `quotientEquivSelf`, `RightAddCosetEquivalence`, `RightCosetEquivalence`, `groupEquivQuotientProdSubgroup`, `leftCosetEquivSubgroup`, `quotientEquivProdOfLE`, `quotientEquivProdOfLE'`, `quotientMapOfLE`, `quotientSubgroupOfEmbeddingOfLE`, `quotientSubgroupOfMapOfLE`, `quotientiInfEmbedding`, `quotientiInfSubgroupOfEmbedding`, `rightCosetEquivSubgroup`	36
Theorems `fiberEquivKer_apply`, `fiberEquivKer_symm_apply`, `fiberEquiv_apply`, `fiberEquiv_symm_apply`, `quotientAddSubgroupOfEmbeddingOfLE_apply_mk`, `quotientAddSubgroupOfMapOfLE_apply_mk`, `quotientEquivProdOfLE'_apply`, `quotientEquivProdOfLE'_symm_apply`, `quotientEquivProdOfLE_apply`, `quotientEquivProdOfLE_symm_apply`, `quotientMapOfLE_apply_mk`, `quotientiInfAddSubgroupOfEmbedding_apply`, `quotientiInfAddSubgroupOfEmbedding_apply_mk`, `quotientiInfEmbedding_apply`, `quotientiInfEmbedding_apply_mk`, `fiberEquivKer_apply`, `fiberEquivKer_symm_apply`, `fiberEquiv_apply`, `fiberEquiv_symm_apply`, `eq_class_eq_leftCoset`, `leftRel_pi`, `leftRel_prod`, `orbit_eq_out_vadd`, `orbit_mk_eq_vadd`, `rightRel_pi`, `rightRel_prod`, `strictMono_comap_prod_image`, `univ_eq_iUnion_vadd`, `eq_class_eq_leftCoset`, `leftRel_pi`, `leftRel_prod`, `leftRel_r_eq_leftCosetEquivalence`, `orbit_eq_out_smul`, `orbit_mk_eq_smul`, `rightRel_pi`, `rightRel_prod`, `rightRel_r_eq_rightCosetEquivalence`, `strictMono_comap_prod_image`, `univ_eq_iUnion_smul`, `quotientEquivProdOfLE'_apply`, `quotientEquivProdOfLE'_symm_apply`, `quotientEquivProdOfLE_apply`, `quotientEquivProdOfLE_symm_apply`, `quotientMapOfLE_apply_mk`, `quotientSubgroupOfEmbeddingOfLE_apply_mk`, `quotientSubgroupOfMapOfLE_apply_mk`, `quotientiInfEmbedding_apply`, `quotientiInfEmbedding_apply_mk`, `quotientiInfSubgroupOfEmbedding_apply`, `quotientiInfSubgroupOfEmbedding_apply_mk`, `eq_addCosets_of_normal`, `eq_cosets_of_normal`, `leftAddCosetEquivalence_rel`, `leftAddCoset_assoc`, `leftAddCoset_eq_iff`, `leftAddCoset_mem_leftAddCoset`, `leftAddCoset_rightAddCoset`, `leftCosetEquivalence_rel`, `leftCoset_assoc`, `leftCoset_eq_iff`, `leftCoset_mem_leftCoset`, `leftCoset_rightCoset`, `mem_leftAddCoset`, `mem_leftAddCoset_iff`, `mem_leftAddCoset_leftAddCoset`, `mem_leftCoset`, `mem_leftCoset_iff`, `mem_leftCoset_leftCoset`, `mem_own_leftAddCoset`, `mem_own_leftCoset`, `mem_own_rightAddCoset`, `mem_own_rightCoset`, `mem_rightAddCoset`, `mem_rightAddCoset_iff`, `mem_rightAddCoset_rightAddCoset`, `mem_rightCoset`, `mem_rightCoset_iff`, `mem_rightCoset_rightCoset`, `normal_iff_eq_addCosets`, `normal_iff_eq_cosets`, `normal_of_eq_addCosets`, `normal_of_eq_cosets`, `one_leftCoset`, `orbit_addSubgroup_eq_rightCoset`, `orbit_addSubgroup_eq_self_of_mem`, `orbit_addSubgroup_zero_eq_self`, `orbit_subgroup_eq_rightCoset`, `orbit_subgroup_eq_self_of_mem`, `orbit_subgroup_one_eq_self`, `rightAddCosetEquivalence_rel`, `rightAddCoset_assoc`, `rightAddCoset_eq_iff`, `rightAddCoset_mem_rightAddCoset`, `rightAddCoset_zero`, `rightCosetEquivalence_rel`, `rightCoset_assoc`, `rightCoset_eq_iff`, `rightCoset_mem_rightCoset`, `rightCoset_one`, `zero_leftAddCoset`	100
Total	136

AddMonoidHom

Definitions

Name	Category	Theorems
`fiberEquiv` 📖	CompOp	2 math math: `fiberEquiv_symm_apply`, `fiberEquiv_apply`
`fiberEquivKer` 📖	CompOp	2 math math: `fiberEquivKer_apply`, `fiberEquivKer_symm_apply`
`fiberEquivKerOfSurjective` 📖	CompOp	—
`fiberEquivOfSurjective` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fiberEquivKer_apply` 📖	mathematical	—	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `ker` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DFunLike.coe` `Equiv` `Set.Elem` `Set.preimage` `AddMonoidHom` `AddZeroClass.toAddZero` `instFunLike` `Set` `Set.instSingletonSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `fiberEquivKer` `AddZero.toAdd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Set.instMembership`	—	—
`fiberEquivKer_symm_apply` 📖	mathematical	—	`Set` `Set.instMembership` `Set.preimage` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLike` `Set.instSingletonSet` `Equiv` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `ker` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `fiberEquivKer` `AddZero.toAdd`	—	—
`fiberEquiv_apply` 📖	mathematical	—	`Set` `Set.instMembership` `Set.preimage` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLike` `Set.instSingletonSet` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `fiberEquiv` `AddZero.toAdd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`fiberEquiv_symm_apply` 📖	mathematical	—	`Set` `Set.instMembership` `Set.preimage` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLike` `Set.instSingletonSet` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `fiberEquiv` `AddZero.toAdd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—

AddSubgroup

Definitions

Name	Category	Theorems
`addGroupEquivQuotientProdAddSubgroup` 📖	CompOp	—
`leftCosetEquivAddSubgroup` 📖	CompOp	—
`quotientAddSubgroupOfEmbeddingOfLE` 📖	CompOp	1 math math: `quotientAddSubgroupOfEmbeddingOfLE_apply_mk`
`quotientAddSubgroupOfMapOfLE` 📖	CompOp	2 math math: `quotientAddSubgroupOfMapOfLE_apply_mk`, `quotientiInfAddSubgroupOfEmbedding_apply`
`quotientEquivProdOfLE` 📖	CompOp	2 math math: `quotientEquivProdOfLE_symm_apply`, `quotientEquivProdOfLE_apply`
`quotientEquivProdOfLE'` 📖	CompOp	2 math math: `quotientEquivProdOfLE'_apply`, `quotientEquivProdOfLE'_symm_apply`
`quotientMapOfLE` 📖	CompOp	2 math math: `quotientiInfEmbedding_apply`, `quotientMapOfLE_apply_mk`
`quotientiInfAddSubgroupOfEmbedding` 📖	CompOp	2 math math: `quotientiInfAddSubgroupOfEmbedding_apply_mk`, `quotientiInfAddSubgroupOfEmbedding_apply`
`quotientiInfEmbedding` 📖	CompOp	2 math math: `quotientiInfEmbedding_apply_mk`, `quotientiInfEmbedding_apply`
`rightCosetEquivAddSubgroup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quotientAddSubgroupOfEmbeddingOfLE_apply_mk` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`DFunLike.coe` `Function.Embedding` `HasQuotient.Quotient` `SetLike.instMembership` `instSetLike` `toAddGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `addSubgroupOf` `Function.instFunLikeEmbedding` `quotientAddSubgroupOfEmbeddingOfLE` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `inclusion`	—	—
`quotientAddSubgroupOfMapOfLE_apply_mk` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`quotientAddSubgroupOfMapOfLE` `SetLike.instMembership` `instSetLike` `toAddGroup` `addSubgroupOf`	—	—
`quotientEquivProdOfLE'_apply` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `HasQuotient.Quotient` `QuotientAddGroup.instHasQuotientAddSubgroup`	`DFunLike.coe` `Equiv` `SetLike.instMembership` `instSetLike` `toAddGroup` `addSubgroupOf` `EquivLike.toFunLike` `Equiv.instEquivLike` `quotientEquivProdOfLE'` `Quotient.map'` `QuotientAddGroup.leftRel` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Quotient.mk''`	—	—
`quotientEquivProdOfLE'_symm_apply` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `HasQuotient.Quotient` `QuotientAddGroup.instHasQuotientAddSubgroup`	`DFunLike.coe` `Equiv` `SetLike.instMembership` `instSetLike` `toAddGroup` `addSubgroupOf` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `quotientEquivProdOfLE'` `Quotient.map'` `QuotientAddGroup.leftRel` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—
`quotientEquivProdOfLE_apply` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`DFunLike.coe` `Equiv` `HasQuotient.Quotient` `QuotientAddGroup.instHasQuotientAddSubgroup` `SetLike.instMembership` `instSetLike` `toAddGroup` `addSubgroupOf` `EquivLike.toFunLike` `Equiv.instEquivLike` `quotientEquivProdOfLE` `Quotient.map'` `QuotientAddGroup.leftRel` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Quotient.out` `Quotient.mk''`	—	—
`quotientEquivProdOfLE_symm_apply` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`DFunLike.coe` `Equiv` `HasQuotient.Quotient` `QuotientAddGroup.instHasQuotientAddSubgroup` `SetLike.instMembership` `instSetLike` `toAddGroup` `addSubgroupOf` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `quotientEquivProdOfLE` `Quotient.map'` `QuotientAddGroup.leftRel` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.out`	—	—
`quotientMapOfLE_apply_mk` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`quotientMapOfLE`	—	—
`quotientiInfAddSubgroupOfEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `HasQuotient.Quotient` `AddSubgroup` `SetLike.instMembership` `instSetLike` `toAddGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `addSubgroupOf` `iInf` `instInfSet` `Function.instFunLikeEmbedding` `quotientiInfAddSubgroupOfEmbedding` `quotientAddSubgroupOfMapOfLE` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `instCompleteLattice`	—	—
`quotientiInfAddSubgroupOfEmbedding_apply_mk` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `HasQuotient.Quotient` `AddSubgroup` `SetLike.instMembership` `instSetLike` `toAddGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `addSubgroupOf` `iInf` `instInfSet` `Function.instFunLikeEmbedding` `quotientiInfAddSubgroupOfEmbedding`	—	—
`quotientiInfEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `HasQuotient.Quotient` `AddSubgroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `iInf` `instInfSet` `Function.instFunLikeEmbedding` `quotientiInfEmbedding` `quotientMapOfLE` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `instCompleteLattice`	—	—
`quotientiInfEmbedding_apply_mk` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `HasQuotient.Quotient` `AddSubgroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `iInf` `instInfSet` `Function.instFunLikeEmbedding` `quotientiInfEmbedding`	—	—

MonoidHom

Definitions

Name	Category	Theorems
`fiberEquiv` 📖	CompOp	2 math math: `fiberEquiv_symm_apply`, `fiberEquiv_apply`
`fiberEquivKer` 📖	CompOp	2 math math: `fiberEquivKer_symm_apply`, `fiberEquivKer_apply`
`fiberEquivKerOfSurjective` 📖	CompOp	—
`fiberEquivOfSurjective` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fiberEquivKer_apply` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `ker` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DFunLike.coe` `Equiv` `Set.Elem` `Set.preimage` `MonoidHom` `MulOneClass.toMulOne` `instFunLike` `Set` `Set.instSingletonSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `fiberEquivKer` `MulOne.toMul` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Set.instMembership`	—	—
`fiberEquivKer_symm_apply` 📖	mathematical	—	`Set` `Set.instMembership` `Set.preimage` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instFunLike` `Set.instSingletonSet` `Equiv` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `ker` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `fiberEquivKer` `MulOne.toMul`	—	—
`fiberEquiv_apply` 📖	mathematical	—	`Set` `Set.instMembership` `Set.preimage` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instFunLike` `Set.instSingletonSet` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `fiberEquiv` `MulOne.toMul` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`fiberEquiv_symm_apply` 📖	mathematical	—	`Set` `Set.instMembership` `Set.preimage` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instFunLike` `Set.instSingletonSet` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `fiberEquiv` `MulOne.toMul` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—

QuotientAddGroup

Definitions

Name	Category	Theorems
`preimageMkEquivAddSubgroupProdSet` 📖	CompOp	—
`quotientEquivSelf` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_class_eq_leftCoset` 📖	mathematical	—	`setOf` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `SetLike.coe` `AddSubgroup.instSetLike`	—	`Set.ext` `mem_leftAddCoset_iff` `Set.mem_setOf_eq` `eq` `SetLike.mem_coe`
`leftRel_pi` 📖	mathematical	—	`leftRel` `Pi.addGroup` `AddSubgroup.pi` `Set.univ` `piSetoid`	—	`Setoid.ext` `leftRel_apply` `AddSubgroup.mem_pi` `Set.mem_univ` `Setoid.piSetoid_apply`
`leftRel_prod` 📖	mathematical	—	`leftRel` `Prod.instAddGroup` `AddSubgroup.prod` `Setoid.prod`	—	`Setoid.ext` `Setoid.prod_apply` `leftRel_apply`
`orbit_eq_out_vadd` 📖	mathematical	—	`AddAction.orbitRel.Quotient.orbit` `AddOpposite` `AddSubgroup` `AddOpposite.instAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.op` `AddSubgroup.toAddGroup` `AddAction.instAddAction` `AddMonoid.toOppositeAddAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `Quotient.out` `leftRel` `SetLike.coe`	—	`induction_on` `orbit_mk_eq_vadd` `eq_class_eq_leftCoset` `Quotient.out_eq'`
`orbit_mk_eq_vadd` 📖	mathematical	—	`AddAction.orbitRel.Quotient.orbit` `AddOpposite` `AddSubgroup` `AddOpposite.instAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.op` `AddSubgroup.toAddGroup` `AddAction.instAddAction` `AddMonoid.toOppositeAddAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `SetLike.coe`	—	`Set.ext` `AddAction.orbitRel.Quotient.mem_orbit` `Quotient.eq''` `Set.mem_vadd_set_iff_neg_vadd_mem` `SetLike.mem_coe` `leftRel_apply` `Setoid.comm'`
`rightRel_pi` 📖	mathematical	—	`rightRel` `Pi.addGroup` `AddSubgroup.pi` `Set.univ` `piSetoid`	—	`Setoid.ext` `rightRel_apply` `AddSubgroup.mem_pi` `Set.mem_univ` `Setoid.piSetoid_apply`
`rightRel_prod` 📖	mathematical	—	`rightRel` `Prod.instAddGroup` `AddSubgroup.prod` `Setoid.prod`	—	`Setoid.ext` `Setoid.prod_apply` `rightRel_apply`
`strictMono_comap_prod_image` 📖	mathematical	—	`StrictMono` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.toAddGroup` `Set` `HasQuotient.Quotient` `instHasQuotientAddSubgroup` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `Prod.instPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `AddSubgroup.comap` `AddSubgroup.subtype` `Set.image` `SetLike.coe`	—	`AddSubgroup.comap_mono` `Set.image_mono` `eq` `add_neg_cancel_left` `AddSubgroup.add_mem` `AddSubgroup.neg_mem`
`univ_eq_iUnion_vadd` 📖	mathematical	—	`Set.univ` `Set.iUnion` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `Quotient.out` `leftRel` `SetLike.coe` `AddSubgroup.instSetLike`	—	`AddAction.univ_eq_iUnion_orbit` `orbit_eq_out_vadd`

QuotientGroup

Definitions

Name	Category	Theorems
`preimageMkEquivSubgroupProdSet` 📖	CompOp	—
`quotientEquivSelf` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_class_eq_leftCoset` 📖	mathematical	—	`setOf` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Subgroup.instSetLike`	—	`Set.ext` `mem_leftCoset_iff` `Set.mem_setOf_eq` `eq` `SetLike.mem_coe`
`leftRel_pi` 📖	mathematical	—	`leftRel` `Pi.group` `Subgroup.pi` `Set.univ` `piSetoid`	—	`Setoid.ext`
`leftRel_prod` 📖	mathematical	—	`leftRel` `Prod.instGroup` `Subgroup.prod` `Setoid.prod`	—	`Setoid.ext` `Setoid.prod_apply`
`leftRel_r_eq_leftCosetEquivalence` 📖	mathematical	—	`leftRel` `LeftCosetEquivalence` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	—	`leftRel_eq` `leftCoset_eq_iff`
`orbit_eq_out_smul` 📖	mathematical	—	`MulAction.orbitRel.Quotient.orbit` `MulOpposite` `Subgroup` `MulOpposite.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.op` `Subgroup.toGroup` `MulAction.instMulAction` `Monoid.toOppositeMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `Quotient.out` `leftRel` `SetLike.coe`	—	`induction_on` `orbit_mk_eq_smul` `Quotient.out_eq'`
`orbit_mk_eq_smul` 📖	mathematical	—	`MulAction.orbitRel.Quotient.orbit` `MulOpposite` `Subgroup` `MulOpposite.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.op` `Subgroup.toGroup` `MulAction.instMulAction` `Monoid.toOppositeMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe`	—	`Set.ext` `MulAction.orbitRel.Quotient.mem_orbit` `Setoid.comm'`
`rightRel_pi` 📖	mathematical	—	`rightRel` `Pi.group` `Subgroup.pi` `Set.univ` `piSetoid`	—	`Setoid.ext`
`rightRel_prod` 📖	mathematical	—	`rightRel` `Prod.instGroup` `Subgroup.prod` `Setoid.prod`	—	`Setoid.ext` `Setoid.prod_apply`
`rightRel_r_eq_rightCosetEquivalence` 📖	mathematical	—	`rightRel` `RightCosetEquivalence` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	—	`rightRel_eq` `rightCoset_eq_iff`
`strictMono_comap_prod_image` 📖	mathematical	—	`StrictMono` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Set` `HasQuotient.Quotient` `instHasQuotientSubgroup` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Prod.instPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Subgroup.comap` `Subgroup.subtype` `Set.image` `SetLike.coe`	—	`Subgroup.comap_mono` `Set.image_mono` `eq` `mul_inv_cancel_left` `Subgroup.mul_mem` `Subgroup.inv_mem`
`univ_eq_iUnion_smul` 📖	mathematical	—	`Set.univ` `Set.iUnion` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `Quotient.out` `leftRel` `SetLike.coe` `Subgroup.instSetLike`	—	`MulAction.univ_eq_iUnion_orbit` `orbit_eq_out_smul`

Subgroup

Definitions

Name	Category	Theorems
`groupEquivQuotientProdSubgroup` 📖	CompOp	—
`leftCosetEquivSubgroup` 📖	CompOp	—
`quotientEquivProdOfLE` 📖	CompOp	2 math math: `quotientEquivProdOfLE_apply`, `quotientEquivProdOfLE_symm_apply`
`quotientEquivProdOfLE'` 📖	CompOp	2 math math: `quotientEquivProdOfLE'_symm_apply`, `quotientEquivProdOfLE'_apply`
`quotientMapOfLE` 📖	CompOp	2 math math: `quotientiInfEmbedding_apply`, `quotientMapOfLE_apply_mk`
`quotientSubgroupOfEmbeddingOfLE` 📖	CompOp	1 math math: `quotientSubgroupOfEmbeddingOfLE_apply_mk`
`quotientSubgroupOfMapOfLE` 📖	CompOp	2 math math: `quotientSubgroupOfMapOfLE_apply_mk`, `quotientiInfSubgroupOfEmbedding_apply`
`quotientiInfEmbedding` 📖	CompOp	2 math math: `quotientiInfEmbedding_apply_mk`, `quotientiInfEmbedding_apply`
`quotientiInfSubgroupOfEmbedding` 📖	CompOp	2 math math: `quotientiInfSubgroupOfEmbedding_apply_mk`, `quotientiInfSubgroupOfEmbedding_apply`
`rightCosetEquivSubgroup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quotientEquivProdOfLE'_apply` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup`	`DFunLike.coe` `Equiv` `SetLike.instMembership` `instSetLike` `toGroup` `subgroupOf` `EquivLike.toFunLike` `Equiv.instEquivLike` `quotientEquivProdOfLE'` `Quotient.map'` `QuotientGroup.leftRel` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Quotient.mk''`	—	—
`quotientEquivProdOfLE'_symm_apply` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup`	`DFunLike.coe` `Equiv` `SetLike.instMembership` `instSetLike` `toGroup` `subgroupOf` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `quotientEquivProdOfLE'` `Quotient.map'` `QuotientGroup.leftRel` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`quotientEquivProdOfLE_apply` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`DFunLike.coe` `Equiv` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup` `SetLike.instMembership` `instSetLike` `toGroup` `subgroupOf` `EquivLike.toFunLike` `Equiv.instEquivLike` `quotientEquivProdOfLE` `Quotient.map'` `QuotientGroup.leftRel` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Quotient.out` `Quotient.mk''`	—	—
`quotientEquivProdOfLE_symm_apply` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`DFunLike.coe` `Equiv` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup` `SetLike.instMembership` `instSetLike` `toGroup` `subgroupOf` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `quotientEquivProdOfLE` `Quotient.map'` `QuotientGroup.leftRel` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.out`	—	—
`quotientMapOfLE_apply_mk` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`quotientMapOfLE`	—	—
`quotientSubgroupOfEmbeddingOfLE_apply_mk` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`DFunLike.coe` `Function.Embedding` `HasQuotient.Quotient` `SetLike.instMembership` `instSetLike` `toGroup` `QuotientGroup.instHasQuotientSubgroup` `subgroupOf` `Function.instFunLikeEmbedding` `quotientSubgroupOfEmbeddingOfLE` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `inclusion`	—	—
`quotientSubgroupOfMapOfLE_apply_mk` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`quotientSubgroupOfMapOfLE` `SetLike.instMembership` `instSetLike` `toGroup` `subgroupOf`	—	—
`quotientiInfEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `iInf` `instInfSet` `Function.instFunLikeEmbedding` `quotientiInfEmbedding` `quotientMapOfLE` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `instCompleteLattice`	—	—
`quotientiInfEmbedding_apply_mk` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `iInf` `instInfSet` `Function.instFunLikeEmbedding` `quotientiInfEmbedding`	—	—
`quotientiInfSubgroupOfEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `HasQuotient.Quotient` `Subgroup` `SetLike.instMembership` `instSetLike` `toGroup` `QuotientGroup.instHasQuotientSubgroup` `subgroupOf` `iInf` `instInfSet` `Function.instFunLikeEmbedding` `quotientiInfSubgroupOfEmbedding` `quotientSubgroupOfMapOfLE` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `instCompleteLattice`	—	—
`quotientiInfSubgroupOfEmbedding_apply_mk` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `HasQuotient.Quotient` `Subgroup` `SetLike.instMembership` `instSetLike` `toGroup` `QuotientGroup.instHasQuotientSubgroup` `subgroupOf` `iInf` `instInfSet` `Function.instFunLikeEmbedding` `quotientiInfSubgroupOfEmbedding`	—	—

(root)

Definitions

Name	Category	Theorems
`LeftAddCosetEquivalence` 📖	MathDef	1 math math: `leftAddCosetEquivalence_rel`
`LeftCosetEquivalence` 📖	MathDef	4 math math: `Subgroup.IsComplement.equiv_fst_eq_iff_leftCosetEquivalence`, `QuotientGroup.leftRel_r_eq_leftCosetEquivalence`, `Subgroup.IsComplement.leftCosetEquivalence_equiv_fst`, `leftCosetEquivalence_rel`
`RightAddCosetEquivalence` 📖	MathDef	1 math math: `rightAddCosetEquivalence_rel`
`RightCosetEquivalence` 📖	MathDef	4 math math: `Subgroup.IsComplement.equiv_snd_eq_iff_rightCosetEquivalence`, `QuotientGroup.rightRel_r_eq_rightCosetEquivalence`, `Subgroup.IsComplement.rightCosetEquivalence_equiv_snd`, `rightCosetEquivalence_rel`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_addCosets_of_normal` 📖	mathematical	—	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `AddOpposite` `AddOpposite.instAddMonoid` `AddMonoid.toOppositeAddAction` `AddOpposite.op`	—	`Set.ext` `mem_leftAddCoset_iff` `SetLike.mem_coe` `AddSubgroup.Normal.mem_comm_iff` `mem_rightAddCoset_iff`
`eq_cosets_of_normal` 📖	mathematical	—	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `MulOpposite` `MulOpposite.instMonoid` `Monoid.toOppositeMulAction` `MulOpposite.op`	—	`Set.ext` `Subgroup.Normal.mem_comm_iff`
`leftAddCosetEquivalence_rel` 📖	mathematical	—	`LeftAddCosetEquivalence`	—	—
`leftAddCoset_assoc` 📖	mathematical	—	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `Add.toVAdd` `AddSemigroup.toAdd`	—	`Set.image_congr` `Set.image_comp` `add_assoc`
`leftAddCoset_eq_iff` 📖	mathematical	—	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `SetLike.instMembership` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Set.ext_iff` `mem_leftAddCoset_iff` `SetLike.mem_coe` `neg_add_cancel` `AddSubgroup.zero_mem` `add_neg_cancel_right` `add_assoc` `AddSubgroup.add_mem_cancel_left`
`leftAddCoset_mem_leftAddCoset` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `SetLike.coe`	—	`Set.ext` `mem_leftAddCoset_iff` `SetLike.mem_coe` `add_mem_cancel_left` `AddSubgroup.instAddSubgroupClass` `AddSubgroup.neg_mem`
`leftAddCoset_rightAddCoset` 📖	mathematical	—	`HVAdd.hVAdd` `AddOpposite` `Set` `instHVAdd` `Set.vaddSet` `Add.toVAddAddOpposite` `AddSemigroup.toAdd` `AddOpposite.op` `Add.toVAdd`	—	`Set.image_congr` `Set.image_comp` `add_assoc`
`leftCosetEquivalence_rel` 📖	mathematical	—	`LeftCosetEquivalence`	—	—
`leftCoset_assoc` 📖	mathematical	—	`Set` `Set.smulSet` `Semigroup.toMul`	—	`Set.image_congr` `Set.image_comp` `mul_assoc`
`leftCoset_eq_iff` 📖	mathematical	—	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `SetLike.instMembership` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Set.ext_iff` `inv_mul_cancel` `Subgroup.one_mem` `mul_inv_cancel_right` `mul_assoc` `Subgroup.mul_mem_cancel_left`
`leftCoset_mem_leftCoset` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike`	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe`	—	`Set.ext` `mul_mem_cancel_left` `Subgroup.instSubgroupClass` `Subgroup.inv_mem`
`leftCoset_rightCoset` 📖	mathematical	—	`MulOpposite` `Set` `Set.smulSet` `Mul.toSMulMulOpposite` `Semigroup.toMul` `MulOpposite.op`	—	`Set.image_congr` `Set.image_comp` `mul_assoc`
`mem_leftAddCoset` 📖	mathematical	`Set` `Set.instMembership`	`HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `Add.toVAdd`	—	`Set.mem_image_of_mem`
`mem_leftAddCoset_iff` 📖	mathematical	—	`Set` `Set.instMembership` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`neg_add_cancel_left` `add_neg_cancel_left`
`mem_leftAddCoset_leftAddCoset` 📖	mathematical	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `SetLike.coe` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddSubmonoid.instSetLike`	`SetLike.instMembership`	—	`SetLike.mem_coe` `mem_own_leftAddCoset`
`mem_leftCoset` 📖	mathematical	`Set` `Set.instMembership`	`Set.smulSet`	—	`Set.mem_image_of_mem`
`mem_leftCoset_iff` 📖	mathematical	—	`Set` `Set.instMembership` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`inv_mul_cancel_left` `mul_inv_cancel_left`
`mem_leftCoset_leftCoset` 📖	mathematical	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Submonoid` `Monoid.toMulOneClass` `Submonoid.instSetLike`	`SetLike.instMembership`	—	`SetLike.mem_coe` `mem_own_leftCoset`
`mem_own_leftAddCoset` 📖	mathematical	—	`Set` `Set.instMembership` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `SetLike.coe` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddSubmonoid.instSetLike`	—	`mem_leftAddCoset` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubmonoid.instAddSubmonoidClass` `add_zero`
`mem_own_leftCoset` 📖	mathematical	—	`Set` `Set.instMembership` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Submonoid` `Monoid.toMulOneClass` `Submonoid.instSetLike`	—	`mem_leftCoset` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `mul_one`
`mem_own_rightAddCoset` 📖	mathematical	—	`Set` `Set.instMembership` `HVAdd.hVAdd` `AddOpposite` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddOpposite.instAddMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toOppositeAddAction` `AddOpposite.op` `SetLike.coe` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddSubmonoid.instSetLike`	—	`mem_rightAddCoset` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubmonoid.instAddSubmonoidClass` `zero_add`
`mem_own_rightCoset` 📖	mathematical	—	`Set` `Set.instMembership` `MulOpposite` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulOpposite.instMonoid` `MulAction.toSemigroupAction` `Monoid.toOppositeMulAction` `MulOpposite.op` `SetLike.coe` `Submonoid` `Monoid.toMulOneClass` `Submonoid.instSetLike`	—	`mem_rightCoset` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `one_mul`
`mem_rightAddCoset` 📖	mathematical	`Set` `Set.instMembership`	`HVAdd.hVAdd` `AddOpposite` `instHVAdd` `Set.vaddSet` `Add.toVAddAddOpposite` `AddOpposite.op`	—	`Set.mem_image_of_mem`
`mem_rightAddCoset_iff` 📖	mathematical	—	`Set` `Set.instMembership` `HVAdd.hVAdd` `AddOpposite` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddOpposite.instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toOppositeAddAction` `AddOpposite.op` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`add_neg_cancel_right` `neg_add_cancel_right`
`mem_rightAddCoset_rightAddCoset` 📖	mathematical	`HVAdd.hVAdd` `AddOpposite` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddOpposite.instAddMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toOppositeAddAction` `AddOpposite.op` `SetLike.coe` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddSubmonoid.instSetLike`	`SetLike.instMembership`	—	`SetLike.mem_coe` `mem_own_rightAddCoset`
`mem_rightCoset` 📖	mathematical	`Set` `Set.instMembership`	`MulOpposite` `Set.smulSet` `Mul.toSMulMulOpposite` `MulOpposite.op`	—	`Set.mem_image_of_mem`
`mem_rightCoset_iff` 📖	mathematical	—	`Set` `Set.instMembership` `MulOpposite` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulOpposite.instMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toOppositeMulAction` `MulOpposite.op` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`mul_inv_cancel_right` `inv_mul_cancel_right`
`mem_rightCoset_rightCoset` 📖	mathematical	`MulOpposite` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulOpposite.instMonoid` `MulAction.toSemigroupAction` `Monoid.toOppositeMulAction` `MulOpposite.op` `SetLike.coe` `Submonoid` `Monoid.toMulOneClass` `Submonoid.instSetLike`	`SetLike.instMembership`	—	`SetLike.mem_coe` `mem_own_rightCoset`
`normal_iff_eq_addCosets` 📖	mathematical	—	`AddSubgroup.Normal` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `AddOpposite` `AddOpposite.instAddMonoid` `AddMonoid.toOppositeAddAction` `AddOpposite.op`	—	`eq_addCosets_of_normal` `normal_of_eq_addCosets`
`normal_iff_eq_cosets` 📖	mathematical	—	`Subgroup.Normal` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `MulOpposite` `MulOpposite.instMonoid` `Monoid.toOppositeMulAction` `MulOpposite.op`	—	`eq_cosets_of_normal` `normal_of_eq_cosets`
`normal_of_eq_addCosets` 📖	mathematical	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `AddOpposite` `AddOpposite.instAddMonoid` `AddMonoid.toOppositeAddAction` `AddOpposite.op`	`AddSubgroup.Normal`	—	`mem_rightAddCoset_iff` `mem_leftAddCoset`
`normal_of_eq_cosets` 📖	mathematical	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `MulOpposite` `MulOpposite.instMonoid` `Monoid.toOppositeMulAction` `MulOpposite.op`	`Subgroup.Normal`	—	`mem_rightCoset_iff` `mem_leftCoset`
`one_leftCoset` 📖	mathematical	—	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`Set.ext` `one_smul`
`orbit_addSubgroup_eq_rightCoset` 📖	mathematical	—	`AddAction.orbit` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddAction.instAddAction` `AddMonoid.toAddAction` `HVAdd.hVAdd` `AddOpposite` `Set` `instHVAdd` `Set.vaddSet` `AddOpposite.instAddMonoid` `AddMonoid.toOppositeAddAction` `AddOpposite.op` `SetLike.coe`	—	`Set.ext`
`orbit_addSubgroup_eq_self_of_mem` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike`	`AddAction.orbit` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddAction.instAddAction` `AddMonoid.toAddAction` `SetLike.coe`	—	`orbit_addSubgroup_eq_rightCoset` `rightAddCoset_mem_rightAddCoset`
`orbit_addSubgroup_zero_eq_self` 📖	mathematical	—	`AddAction.orbit` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddAction.instAddAction` `AddMonoid.toAddAction` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SetLike.coe`	—	`orbit_addSubgroup_eq_self_of_mem` `AddSubgroup.zero_mem`
`orbit_subgroup_eq_rightCoset` 📖	mathematical	—	`MulAction.orbit` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `MulAction.instMulAction` `Monoid.toMulAction` `MulOpposite` `Set` `Set.smulSet` `MulOpposite.instMonoid` `Monoid.toOppositeMulAction` `MulOpposite.op` `SetLike.coe`	—	`Set.ext`
`orbit_subgroup_eq_self_of_mem` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike`	`MulAction.orbit` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `MulAction.instMulAction` `Monoid.toMulAction` `SetLike.coe`	—	`orbit_subgroup_eq_rightCoset` `rightCoset_mem_rightCoset`
`orbit_subgroup_one_eq_self` 📖	mathematical	—	`MulAction.orbit` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `MulAction.instMulAction` `Monoid.toMulAction` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SetLike.coe`	—	`orbit_subgroup_eq_self_of_mem` `Subgroup.one_mem`
`rightAddCosetEquivalence_rel` 📖	mathematical	—	`RightAddCosetEquivalence`	—	—
`rightAddCoset_assoc` 📖	mathematical	—	`HVAdd.hVAdd` `AddOpposite` `Set` `instHVAdd` `Set.vaddSet` `Add.toVAddAddOpposite` `AddSemigroup.toAdd` `AddOpposite.op`	—	`Set.image_congr` `Set.image_comp` `add_assoc`
`rightAddCoset_eq_iff` 📖	mathematical	—	`HVAdd.hVAdd` `AddOpposite` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddOpposite.instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toOppositeAddAction` `AddOpposite.op` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `SetLike.instMembership` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Set.ext_iff` `mem_rightAddCoset_iff` `SetLike.mem_coe` `add_neg_cancel` `AddSubgroup.zero_mem` `neg_add_cancel_left` `add_assoc` `AddSubgroup.add_mem_cancel_right`
`rightAddCoset_mem_rightAddCoset` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike`	`HVAdd.hVAdd` `AddOpposite` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddOpposite.instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toOppositeAddAction` `AddOpposite.op` `SetLike.coe`	—	`Set.ext` `mem_rightAddCoset_iff` `SetLike.mem_coe` `add_mem_cancel_right` `AddSubgroup.instAddSubgroupClass` `AddSubgroup.neg_mem`
`rightAddCoset_zero` 📖	mathematical	—	`HVAdd.hVAdd` `AddOpposite` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddOpposite.instAddMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toOppositeAddAction` `AddOpposite.op` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`Set.ext` `zero_vadd`
`rightCosetEquivalence_rel` 📖	mathematical	—	`RightCosetEquivalence`	—	—
`rightCoset_assoc` 📖	mathematical	—	`MulOpposite` `Set` `Set.smulSet` `Mul.toSMulMulOpposite` `Semigroup.toMul` `MulOpposite.op`	—	`Set.image_congr` `Set.image_comp` `mul_assoc`
`rightCoset_eq_iff` 📖	mathematical	—	`MulOpposite` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulOpposite.instMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toOppositeMulAction` `MulOpposite.op` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `SetLike.instMembership` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Set.ext_iff` `mul_inv_cancel` `Subgroup.one_mem` `inv_mul_cancel_left` `mul_assoc` `Subgroup.mul_mem_cancel_right`
`rightCoset_mem_rightCoset` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike`	`MulOpposite` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulOpposite.instMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toOppositeMulAction` `MulOpposite.op` `SetLike.coe`	—	`Set.ext` `mul_mem_cancel_right` `Subgroup.instSubgroupClass` `Subgroup.inv_mem`
`rightCoset_one` 📖	mathematical	—	`MulOpposite` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulOpposite.instMonoid` `MulAction.toSemigroupAction` `Monoid.toOppositeMulAction` `MulOpposite.op` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`Set.ext` `one_smul`
`zero_leftAddCoset` 📖	mathematical	—	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`Set.ext` `zero_vadd`

---

← Back to Index