Documentation Verification Report

DoubleCoset

📁 Source: Mathlib/GroupTheory/DoubleCoset.lean

Statistics

Metric	Count
Definitions `doubleCoset`, `instInhabitedQuotientCoeSubgroup`, `mk`, `quotToDoubleCoset`, `setoid`	5
Theorems `bot_rel_eq_leftRel`, `disjoint_out`, `doubleCoset_eq_image2`, `doubleCoset_eq_of_mem`, `doubleCoset_union_leftCoset`, `doubleCoset_union_rightCoset`, `eq`, `eq_of_not_disjoint`, `left_bot_eq_left_quot`, `mem_doubleCoset`, `mem_doubleCoset_of_not_disjoint`, `mem_doubleCoset_self`, `mk_eq_of_doubleCoset_eq`, `mk_out_eq_mul`, `out_eq'`, `rel_bot_eq_right_group_rel`, `rel_iff`, `right_bot_eq_right_quot`, `union_quotToDoubleCoset`	19
Total	24

DoubleCoset

Definitions

Name	Category	Theorems
`doubleCoset` 📖	CompOp	6 math math: `doubleCoset_union_rightCoset`, `doubleCoset_eq_image2`, `mem_doubleCoset_self`, `doubleCoset_union_leftCoset`, `mem_doubleCoset`, `disjoint_out`
`instInhabitedQuotientCoeSubgroup` 📖	CompOp	—
`mk` 📖	CompOp	—
`quotToDoubleCoset` 📖	CompOp	1 math math: `union_quotToDoubleCoset`
`setoid` 📖	CompOp	6 math math: `rel_bot_eq_right_group_rel`, `rel_iff`, `disjoint_out`, `bot_rel_eq_leftRel`, `out_eq'`, `mk_out_eq_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_rel_eq_leftRel` 📖	mathematical	—	`setoid` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `Bot.bot` `Subgroup.instBot` `QuotientGroup.leftRel`	—	`rel_iff` `QuotientGroup.leftRel_apply` `one_mul` `inv_mul_cancel_left` `mul_inv_cancel_left`
`disjoint_out` 📖	mathematical	—	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `doubleCoset` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.out` `setoid` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `Quotient.out_eq` `mk_eq_of_doubleCoset_eq` `eq_of_not_disjoint`
`doubleCoset_eq_image2` 📖	mathematical	—	`doubleCoset` `Set.image2`	—	`Set.mul_singleton` `Set.image2_image_left`
`doubleCoset_eq_of_mem` 📖	—	`Set` `Set.instMembership` `doubleCoset` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	—	—	`mem_doubleCoset` `doubleCoset.eq_1` `Set.singleton_mul_singleton` `mul_assoc` `Subgroup.singleton_mul_subgroup` `Subgroup.subgroup_mul_singleton`
`doubleCoset_union_leftCoset` 📖	mathematical	—	`Set.iUnion` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SetLike.coe` `doubleCoset`	—	`Set.ext` `mul_inv_rev` `mul_inv_cancel_right` `mul_inv_cancel` `one_mul` `inv_mul_cancel_right` `inv_mul_cancel`
`doubleCoset_union_rightCoset` 📖	mathematical	—	`Set.iUnion` `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` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SetLike.coe` `doubleCoset`	—	`Set.ext` `mul_inv_rev` `inv_mul_cancel_right` `mul_inv_cancel_right`
`eq` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Quotient.eq''` `rel_iff`
`eq_of_not_disjoint` 📖	—	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `doubleCoset` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	—	—	`mem_doubleCoset_of_not_disjoint` `disjoint_comm` `doubleCoset_eq_of_mem`
`left_bot_eq_left_quot` 📖	mathematical	—	`Quotient` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `Bot.bot` `Subgroup.instBot` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup`	—	`Setoid.ext` `bot_rel_eq_leftRel`
`mem_doubleCoset` 📖	mathematical	—	`Set` `Set.instMembership` `doubleCoset`	—	`doubleCoset_eq_image2`
`mem_doubleCoset_of_not_disjoint` 📖	mathematical	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `doubleCoset` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`Set.instMembership`	—	`Set.not_disjoint_iff` `Subgroup.mul_mem` `Subgroup.inv_mem` `mul_assoc` `eq_inv_mul_iff_mul_eq` `eq_mul_inv_iff_mul_eq`
`mem_doubleCoset_self` 📖	mathematical	—	`Set` `Set.instMembership` `doubleCoset` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	—	`mem_doubleCoset` `Subgroup.one_mem` `one_mul` `mul_one`
`mk_eq_of_doubleCoset_eq` 📖	—	`doubleCoset` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	—	—	`eq` `mem_doubleCoset` `mem_doubleCoset_self`
`mk_out_eq_mul` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Quotient.out` `setoid` `SetLike.coe` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`eq` `out_eq'` `Subgroup.inv_mem` `eq_mul_inv_of_mul_eq` `eq_inv_mul_of_mul_eq` `mul_assoc`
`out_eq'` 📖	mathematical	—	`Quotient.out` `setoid` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	—	`Quotient.out_eq'`
`rel_bot_eq_right_group_rel` 📖	mathematical	—	`setoid` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `Bot.bot` `Subgroup.instBot` `QuotientGroup.rightRel`	—	`rel_iff` `QuotientGroup.rightRel_apply` `mul_one` `mul_inv_cancel_right` `inv_mul_cancel_right`
`rel_iff` 📖	mathematical	—	`setoid` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `SetLike.instMembership` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`mem_doubleCoset_self` `doubleCoset_eq_of_mem` `mem_doubleCoset`
`right_bot_eq_right_quot` 📖	mathematical	—	`Quotient` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `Bot.bot` `Subgroup.instBot` `QuotientGroup.rightRel`	—	`Setoid.ext` `rel_bot_eq_right_group_rel`
`union_quotToDoubleCoset` 📖	mathematical	—	`Set.iUnion` `Quotient` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `quotToDoubleCoset` `Set.univ`	—	`Set.ext` `mk_out_eq_mul` `Subgroup.inv_mem` `inv_mul_cancel` `one_mul` `mul_inv_cancel_right`

---

← Back to Index