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'', eq_of_not_disjoint, finite_quotient_iff_exists_finset_iUnion_eq_univ, iUnion_finset_leftRel_eq_univ_of_leftRel, iUnion_finset_rightRel_eq_univ_of_rightRel, iUnion_image_mk_leftRel, iUnion_image_mk_rightRel, iUnion_quotToDoubleCoset, left_bot_eq_left_quot, mem_doubleCoset, mem_doubleCoset_of_not_disjoint, mem_doubleCoset_self, mem_quotToDoubleCoset_iff, mk_eq_of_doubleCoset_eq, mk_out_eq_mul, out_eq', rel_bot_eq_right_group_rel, rel_iff, right_bot_eq_right_quot	26
Total	31

DoubleCoset

Definitions

Name	Category	Theorems
doubleCoset 📖	CompOp	13 math math: doubleCoset_union_rightCoset, doubleCoset_eq_image2, eq_of_not_disjoint, mem_doubleCoset_self, doubleCoset_union_leftCoset, iUnion_image_mk_rightRel, mem_doubleCoset_of_not_disjoint, iUnion_finset_leftRel_eq_univ_of_leftRel, mem_doubleCoset, disjoint_out, doubleCoset_eq_of_mem, iUnion_finset_rightRel_eq_univ_of_rightRel, iUnion_image_mk_leftRel
instInhabitedQuotientCoeSubgroup 📖	CompOp	—
mk 📖	CompOp	—
quotToDoubleCoset 📖	CompOp	3 math math: finite_quotient_iff_exists_finset_iUnion_eq_univ, iUnion_quotToDoubleCoset, mem_quotToDoubleCoset_iff
setoid 📖	CompOp	11 math math: iUnion_image_mk_rightRel, iUnion_finset_leftRel_eq_univ_of_leftRel, rel_bot_eq_right_group_rel, eq'', rel_iff, disjoint_out, bot_rel_eq_leftRel, out_eq', iUnion_finset_rightRel_eq_univ_of_rightRel, iUnion_image_mk_leftRel, 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 📖	mathematical	Set Set.instMembership doubleCoset MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SetLike.coe Subgroup Subgroup.instSetLike	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	—	eq'' rel_iff
eq'' 📖	mathematical	—	setoid SetLike.coe Subgroup Subgroup.instSetLike	—	Quotient.eq
eq_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	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
finite_quotient_iff_exists_finset_iUnion_eq_univ 📖	mathematical	—	Finite Quotient SetLike.coe Subgroup Subgroup.instSetLike Finset Set.iUnion SetLike.instMembership Finset.instSetLike quotToDoubleCoset Set.univ	—	nonempty_fintype Set.iUnion_congr_Prop Set.iUnion_true iUnion_quotToDoubleCoset Set.eq_univ_iff_forall mem_quotToDoubleCoset_iff Finset.finite_toSet
iUnion_finset_leftRel_eq_univ_of_leftRel 📖	mathematical	Set QuotientGroup.leftRel Set.instHasSubset Set.univ Set.iUnion Quotient SetLike.coe Subgroup Subgroup.instSetLike Finset SetLike.instMembership Finset.instSetLike Set.image doubleCoset MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Quotient.out setoid	Set.iUnion Quotient SetLike.coe Subgroup Subgroup.instSetLike Finset SetLike.instMembership Finset.instSetLike doubleCoset MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Quotient.out setoid Set.univ	—	Mathlib.Tactic.Contrapose.contrapose₁ Set.ne_univ_iff_exists_notMem Mathlib.Tactic.Contrapose.contrapose₄ doubleCoset_eq_of_mem mem_doubleCoset Quotient.eq OneMemClass.one_mem SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass Subgroup.mem_op SubgroupClass.toInvMemClass one_mul eq_mul_inv_of_mul_eq
iUnion_finset_rightRel_eq_univ_of_rightRel 📖	mathematical	Set QuotientGroup.rightRel Set.instHasSubset Set.univ Set.iUnion Quotient SetLike.coe Subgroup Subgroup.instSetLike Finset SetLike.instMembership Finset.instSetLike Set.image doubleCoset MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Quotient.out setoid	Set.iUnion Quotient SetLike.coe Subgroup Subgroup.instSetLike Finset SetLike.instMembership Finset.instSetLike doubleCoset MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Quotient.out setoid Set.univ	—	Mathlib.Tactic.Contrapose.contrapose₁ Set.ne_univ_iff_exists_notMem Mathlib.Tactic.Contrapose.contrapose₄ doubleCoset_eq_of_mem mem_doubleCoset Quotient.eq SubgroupClass.toInvMemClass Subgroup.instSubgroupClass eq_inv_mul_of_mul_eq Subgroup.one_mem mul_one
iUnion_image_mk_leftRel 📖	mathematical	—	Set.iUnion QuotientGroup.leftRel Quotient SetLike.coe Subgroup Subgroup.instSetLike Set.image doubleCoset MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Quotient.out setoid Set.univ	—	iUnion_quotToDoubleCoset Set.iUnion_eq_univ_iff Mathlib.Tactic.Contrapose.contrapose₁ Set.ne_univ_iff_exists_notMem
iUnion_image_mk_rightRel 📖	mathematical	—	Set.iUnion QuotientGroup.rightRel Quotient SetLike.coe Subgroup Subgroup.instSetLike Set.image doubleCoset MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Quotient.out setoid Set.univ	—	iUnion_quotToDoubleCoset Set.iUnion_eq_univ_iff Mathlib.Tactic.Contrapose.contrapose₁ Set.ne_univ_iff_exists_notMem
iUnion_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
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 Set.instMembership doubleCoset MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SetLike.coe Subgroup Subgroup.instSetLike	—	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
mem_quotToDoubleCoset_iff 📖	mathematical	—	Set Set.instMembership quotToDoubleCoset	—	mk_eq_of_doubleCoset_eq doubleCoset_eq_of_mem Quotient.out_eq mem_doubleCoset eq out_eq'
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

---

← Back to Index