Complement

📁 Source: Mathlib/GroupTheory/Complement.lean

Statistics

Metric	Count
Definitions `IsComplement`, `IsComplement'`, `leftQuotientEquiv`, `rightQuotientEquiv`, `toLeftFun`, `toRightFun`, `LeftTransversal`, `RightTransversal`, `instAddActionLeftTransversal`, `instInhabitedLeftTransversal`, `instInhabitedRightTransversal`, `IsComplement`, `IsComplement'`, `QuotientMulEquiv`, `equiv`, `leftQuotientEquiv`, `rightQuotientEquiv`, `toLeftFun`, `toRightFun`, `LeftTransversal`, `RightTransversal`, `instInhabitedLeftTransversal`, `instInhabitedRightTransversal`, `instMulActionLeftTransversal`	24
Theorems `add_eq`, `add_neg_toRightFun_mem`, `card_left`, `card_mul_card`, `card_right`, `encard_left`, `encard_right`, `existsUnique`, `finite_left`, `finite_left_iff`, `finite_right`, `finite_right_iff`, `leftQuotientEquiv_apply`, `mk''_rightQuotientEquiv`, `ncard_left`, `ncard_right`, `neg_add_toLeftFun_mem`, `neg_toLeftFun_add_mem`, `nonempty_left`, `nonempty_right`, `pairwiseDisjoint_vadd`, `quotientAddGroupMk_leftQuotientEquiv`, `rightQuotientEquiv_apply`, `toRightFun_add_neg_mem`, `exists_isComplement_left`, `exists_isComplement_right`, `exists_left_transversal_of_le`, `exists_right_transversal_of_le`, `isComplement'_bot_left`, `isComplement'_bot_right`, `isComplement'_bot_top`, `isComplement'_comm`, `isComplement'_def`, `isComplement'_top_bot`, `isComplement'_top_left`, `isComplement'_top_right`, `isComplement_addSubgroup_left_iff_bijective`, `isComplement_addSubgroup_left_iff_existsUnique_quotientMk''`, `isComplement_addSubgroup_right_iff_bijective`, `isComplement_addSubgroup_right_iff_existsUnique_quotientAddGroupMk`, `isComplement_iff_bijective`, `isComplement_iff_existsUnique`, `isComplement_iff_existsUnique_add_neg_mem`, `isComplement_iff_existsUnique_neg_add_mem`, `isComplement_range_left`, `isComplement_range_right`, `isComplement_singleton_left`, `isComplement_singleton_right`, `isComplement_singleton_univ`, `isComplement_univ_left`, `isComplement_univ_right`, `isComplement_univ_singleton`, `not_isComplement_empty_left`, `not_isComplement_empty_right`, `vadd_apply_eq_vadd_apply_neg_vadd`, `vadd_leftQuotientEquiv`, `vadd_toLeftFun`, `QuotientMulEquiv_apply`, `QuotientMulEquiv_symm_apply`, `card_mul`, `disjoint`, `index_eq_card`, `isCompl`, `sup_eq_top`, `card_left`, `card_mul`, `card_mul_card`, `card_right`, `coe_equiv_fst_eq_one_iff_mem`, `coe_equiv_snd_eq_one_iff_mem`, `encard_left`, `encard_right`, `equiv_fst_eq_iff_leftCosetEquivalence`, `equiv_fst_eq_mul_inv`, `equiv_fst_eq_one_of_mem_of_one_mem`, `equiv_fst_eq_self_iff_mem`, `equiv_fst_eq_self_of_mem_of_one_mem`, `equiv_fst_mul_equiv_snd`, `equiv_mul_left`, `equiv_mul_left_of_mem`, `equiv_mul_right`, `equiv_mul_right_of_mem`, `equiv_one`, `equiv_snd_eq_iff_rightCosetEquivalence`, `equiv_snd_eq_inv_mul`, `equiv_snd_eq_one_of_mem_of_one_mem`, `equiv_snd_eq_self_iff_mem`, `equiv_snd_eq_self_of_mem_of_one_mem`, `equiv_symm_apply`, `existsUnique`, `finite_left`, `finite_left_iff`, `finite_right`, `finite_right_iff`, `inv_mul_toLeftFun_mem`, `inv_toLeftFun_mul_mem`, `leftCosetEquivalence_equiv_fst`, `leftQuotientEquiv_apply`, `mk''_rightQuotientEquiv`, `mul_eq`, `mul_inv_toRightFun_mem`, `ncard_left`, `ncard_right`, `nonempty_left`, `nonempty_right`, `pairwiseDisjoint_smul`, `quotientGroupMk_leftQuotientEquiv`, `rightCosetEquivalence_equiv_snd`, `rightQuotientEquiv_apply`, `toRightFun_mul_inv_mem`, `exists_isComplement_left`, `exists_isComplement_right`, `exists_left_transversal_of_le`, `exists_right_transversal_of_le`, `isComplement'_bot_left`, `isComplement'_bot_right`, `isComplement'_bot_top`, `isComplement'_comm`, `isComplement'_def`, `isComplement'_iff_card_mul_and_disjoint`, `isComplement'_of_card_mul_and_disjoint`, `isComplement'_of_coprime`, `isComplement'_of_disjoint_and_mul_eq_univ`, `isComplement'_stabilizer`, `isComplement'_top_bot`, `isComplement'_top_left`, `isComplement'_top_right`, `isComplement_iff_bijective`, `isComplement_iff_existsUnique`, `isComplement_iff_existsUnique_inv_mul_mem`, `isComplement_iff_existsUnique_mul_inv_mem`, `isComplement_range_left`, `isComplement_range_right`, `isComplement_singleton_left`, `isComplement_singleton_right`, `isComplement_singleton_univ`, `isComplement_subgroup_left_iff_bijective`, `isComplement_subgroup_left_iff_existsUnique_quotientMk''`, `isComplement_subgroup_right_iff_bijective`, `isComplement_subgroup_right_iff_existsUnique_quotientGroupMk`, `isComplement_univ_left`, `isComplement_univ_right`, `isComplement_univ_singleton`, `not_isComplement_empty_left`, `not_isComplement_empty_right`, `smul_apply_eq_smul_apply_inv_smul`, `smul_leftQuotientEquiv`, `smul_toLeftFun`	148
Total	172

AddSubgroup

Definitions

Name	Category	Theorems
`IsComplement` 📖	MathDef	25 math math: `exists_isComplement_left`, `isComplement_iff_bijective`, `isComplement_addSubgroup_left_iff_bijective`, `isComplement_iff_existsUnique_neg_add_mem`, `isComplement_univ_right`, `isComplement_range_left`, `isComplement_addSubgroup_right_iff_bijective`, `isComplement_addSubgroup_right_iff_existsUnique_quotientAddGroupMk`, `vadd_leftQuotientEquiv`, `not_isComplement_empty_right`, `isComplement_addSubgroup_left_iff_existsUnique_quotientMk''`, `isComplement_singleton_univ`, `isComplement_iff_existsUnique`, `isComplement_univ_left`, `exists_isComplement_right`, `vadd_toLeftFun`, `vadd_apply_eq_vadd_apply_neg_vadd`, `isComplement_singleton_left`, `exists_leftTransversal_of_FiniteIndex`, `isComplement'_def`, `isComplement_singleton_right`, `not_isComplement_empty_left`, `isComplement_iff_existsUnique_add_neg_mem`, `isComplement_univ_singleton`, `isComplement_range_right`
`IsComplement'` 📖	MathDef	8 math math: `isComplement'_top_bot`, `isComplement'_top_left`, `isComplement'_top_right`, `isComplement'_comm`, `isComplement'_bot_left`, `isComplement'_def`, `isComplement'_bot_top`, `isComplement'_bot_right`
`LeftTransversal` 📖	CompOp	5 math math: `vadd_leftQuotientEquiv`, `leftTransversals.vadd_diff_vadd`, `vadd_toLeftFun`, `vadd_apply_eq_vadd_apply_neg_vadd`, `AddMonoidHom.transfer_def`
`RightTransversal` 📖	CompOp	—
`instAddActionLeftTransversal` 📖	CompOp	5 math math: `vadd_leftQuotientEquiv`, `leftTransversals.vadd_diff_vadd`, `vadd_toLeftFun`, `vadd_apply_eq_vadd_apply_neg_vadd`, `AddMonoidHom.transfer_def`
`instInhabitedLeftTransversal` 📖	CompOp	—
`instInhabitedRightTransversal` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isComplement_left` 📖	mathematical	—	`IsComplement` `SetLike.coe` `AddSubgroup` `instSetLike` `Set` `Set.instMembership`	—	`isComplement_range_left` `Function.update_self` `Quotient.out_eq'`
`exists_isComplement_right` 📖	mathematical	—	`IsComplement` `SetLike.coe` `AddSubgroup` `instSetLike` `Set` `Set.instMembership`	—	`isComplement_range_right` `Function.update_self` `Quotient.out_eq'`
`exists_left_transversal_of_le` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.coe` `instSetLike` `Nat.card` `Set.Elem` `SetLike.instMembership`	—	`addSubgroupOf_map_subtype` `inf_of_le_left` `exists_isComplement_left` `Set.image_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `IsComplement.add_eq` `Set.image_congr` `Set.image_univ` `Subtype.range_coe_subtype` `IsComplement.card_mul_card` `Nat.card_congr` `subtype_injective`
`exists_right_transversal_of_le` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.coe` `instSetLike` `Nat.card` `SetLike.instMembership` `Set.Elem`	—	`addSubgroupOf_map_subtype` `inf_of_le_left` `exists_isComplement_right` `Set.image_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `IsComplement.add_eq` `Set.image_congr` `Set.image_univ` `Subtype.range_coe_subtype` `IsComplement.card_mul_card` `Nat.card_congr` `subtype_injective`
`isComplement'_bot_left` 📖	mathematical	—	`IsComplement'` `Bot.bot` `AddSubgroup` `instBot` `Top.top` `instTop`	—	`isComplement_singleton_left` `coe_eq_univ`
`isComplement'_bot_right` 📖	mathematical	—	`IsComplement'` `Bot.bot` `AddSubgroup` `instBot` `Top.top` `instTop`	—	`isComplement_singleton_right` `coe_eq_univ`
`isComplement'_bot_top` 📖	mathematical	—	`IsComplement'` `Bot.bot` `AddSubgroup` `instBot` `Top.top` `instTop`	—	`isComplement_singleton_univ`
`isComplement'_comm` 📖	mathematical	—	`IsComplement'`	—	`IsComplement'.symm`
`isComplement'_def` 📖	mathematical	—	`IsComplement'` `IsComplement` `SetLike.coe` `AddSubgroup` `instSetLike`	—	—
`isComplement'_top_bot` 📖	mathematical	—	`IsComplement'` `Top.top` `AddSubgroup` `instTop` `Bot.bot` `instBot`	—	`isComplement_univ_singleton`
`isComplement'_top_left` 📖	mathematical	—	`IsComplement'` `Top.top` `AddSubgroup` `instTop` `Bot.bot` `instBot`	—	`isComplement_univ_left` `coe_eq_singleton`
`isComplement'_top_right` 📖	mathematical	—	`IsComplement'` `Top.top` `AddSubgroup` `instTop` `Bot.bot` `instBot`	—	`isComplement_univ_right` `coe_eq_singleton`
`isComplement_addSubgroup_left_iff_bijective` 📖	mathematical	—	`IsComplement` `SetLike.coe` `AddSubgroup` `instSetLike` `Function.Bijective` `Set.Elem` `QuotientAddGroup.rightRel` `Set.restrict` `Quotient.mk''`	—	`isComplement_addSubgroup_left_iff_existsUnique_quotientMk''` `Function.bijective_iff_existsUnique`
`isComplement_addSubgroup_left_iff_existsUnique_quotientMk''` 📖	mathematical	—	`IsComplement` `SetLike.coe` `AddSubgroup` `instSetLike` `ExistsUnique` `Set.Elem` `QuotientAddGroup.rightRel` `Quotient.mk''` `Set` `Set.instMembership`	—	`isComplement_iff_existsUnique_add_neg_mem` `SetLike.mem_coe` `QuotientAddGroup.rightRel_apply` `Quotient.eq''` `Quotient.forall`
`isComplement_addSubgroup_right_iff_bijective` 📖	mathematical	—	`IsComplement` `SetLike.coe` `AddSubgroup` `instSetLike` `Function.Bijective` `Set.Elem` `HasQuotient.Quotient` `QuotientAddGroup.instHasQuotientAddSubgroup` `Set.restrict`	—	`isComplement_addSubgroup_right_iff_existsUnique_quotientAddGroupMk` `Function.bijective_iff_existsUnique`
`isComplement_addSubgroup_right_iff_existsUnique_quotientAddGroupMk` 📖	mathematical	—	`IsComplement` `SetLike.coe` `AddSubgroup` `instSetLike` `ExistsUnique` `Set.Elem` `HasQuotient.Quotient` `QuotientAddGroup.instHasQuotientAddSubgroup` `Set` `Set.instMembership`	—	`isComplement_iff_existsUnique_neg_add_mem` `SetLike.mem_coe` `QuotientAddGroup.eq`
`isComplement_iff_bijective` 📖	mathematical	—	`IsComplement` `SetLike.coe` `Function.Bijective` `SetLike.instMembership` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—
`isComplement_iff_existsUnique` 📖	mathematical	—	`IsComplement` `ExistsUnique` `Set.Elem` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Set` `Set.instMembership`	—	`Function.bijective_iff_existsUnique`
`isComplement_iff_existsUnique_add_neg_mem` 📖	mathematical	—	`IsComplement` `ExistsUnique` `Set.Elem` `Set` `Set.instMembership` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`neg_add_cancel_right` `add_neg_cancel_right` `Subtype.coe_prop` `isComplement_iff_existsUnique`
`isComplement_iff_existsUnique_neg_add_mem` 📖	mathematical	—	`IsComplement` `ExistsUnique` `Set.Elem` `Set` `Set.instMembership` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`add_neg_cancel_left` `neg_add_cancel_left` `Subtype.coe_prop` `isComplement_iff_existsUnique`
`isComplement_range_left` 📖	mathematical	—	`IsComplement` `Set.range` `HasQuotient.Quotient` `AddSubgroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `SetLike.coe` `instSetLike`	—	`isComplement_addSubgroup_right_iff_bijective`
`isComplement_range_right` 📖	mathematical	`Quotient.mk''` `QuotientAddGroup.rightRel`	`IsComplement` `SetLike.coe` `AddSubgroup` `instSetLike` `Set.range`	—	`isComplement_addSubgroup_left_iff_bijective`
`isComplement_singleton_left` 📖	mathematical	—	`IsComplement` `Set` `Set.instSingletonSet` `Set.univ`	—	`top_le_iff` `add_left_cancel` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `isComplement_singleton_univ`
`isComplement_singleton_right` 📖	mathematical	—	`IsComplement` `Set` `Set.instSingletonSet` `Set.univ`	—	`top_le_iff` `add_right_cancel` `AddRightCancelSemigroup.toIsRightCancelAdd` `isComplement_univ_singleton`
`isComplement_singleton_univ` 📖	mathematical	—	`IsComplement` `Set` `Set.instSingletonSet` `Set.univ`	—	`add_left_cancel` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `add_neg_cancel_left`
`isComplement_univ_left` 📖	mathematical	—	`IsComplement` `Set.univ` `Set` `Set.instSingletonSet`	—	`Set.exists_eq_singleton_iff_nonempty_subsingleton` `mem_top` `neg_add_cancel` `isComplement_univ_singleton`
`isComplement_univ_right` 📖	mathematical	—	`IsComplement` `Set.univ` `Set` `Set.instSingletonSet`	—	`Set.exists_eq_singleton_iff_nonempty_subsingleton` `mem_top` `add_neg_cancel` `isComplement_singleton_univ`
`isComplement_univ_singleton` 📖	mathematical	—	`IsComplement` `Set.univ` `Set` `Set.instSingletonSet`	—	`add_right_cancel` `AddRightCancelSemigroup.toIsRightCancelAdd` `neg_add_cancel_right`
`not_isComplement_empty_left` 📖	mathematical	—	`IsComplement` `Set` `Set.instEmptyCollection`	—	`Set.empty_add` `Set.univ_eq_empty_iff` `not_isEmpty_of_nonempty` `Zero.instNonempty` `IsComplement.add_eq`
`not_isComplement_empty_right` 📖	mathematical	—	`IsComplement` `Set` `Set.instEmptyCollection`	—	`Set.add_empty` `Set.univ_eq_empty_iff` `not_isEmpty_of_nonempty` `Zero.instNonempty` `IsComplement.add_eq`
`vadd_apply_eq_vadd_apply_neg_vadd` 📖	mathematical	—	`Set` `Set.instMembership` `IsComplement` `SetLike.coe` `AddSubgroup` `instSetLike` `HVAdd.hVAdd` `LeftTransversal` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `instAddActionLeftTransversal` `DFunLike.coe` `Equiv` `HasQuotient.Quotient` `QuotientAddGroup.instHasQuotientAddSubgroup` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `IsComplement.leftQuotientEquiv` `AddAction.quotient` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`vadd_leftQuotientEquiv` `vadd_neg_vadd`
`vadd_leftQuotientEquiv` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set` `Set.instMembership` `IsComplement` `SetLike.coe` `AddSubgroup` `instSetLike` `DFunLike.coe` `Equiv` `HasQuotient.Quotient` `QuotientAddGroup.instHasQuotientAddSubgroup` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `IsComplement.leftQuotientEquiv` `LeftTransversal` `instAddActionLeftTransversal` `AddAction.quotient`	—	`Quotient.inductionOn'` `vadd_toLeftFun`
`vadd_toLeftFun` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set` `Set.instMembership` `IsComplement` `SetLike.coe` `AddSubgroup` `instSetLike` `IsComplement.toLeftFun` `LeftTransversal` `instAddActionLeftTransversal`	—	`Set.vadd_mem_vadd_set` `Subtype.coe_prop` `ExistsUnique.unique` `isComplement_iff_existsUnique_neg_add_mem` `AddAction.QuotientAction.inv_mul_mem` `IsComplement.neg_toLeftFun_add_mem`

AddSubgroup.IsComplement

Definitions

Name	Category	Theorems
`leftQuotientEquiv` 📖	CompOp	4 math math: `quotientAddGroupMk_leftQuotientEquiv`, `AddSubgroup.vadd_leftQuotientEquiv`, `AddSubgroup.vadd_apply_eq_vadd_apply_neg_vadd`, `leftQuotientEquiv_apply`
`rightQuotientEquiv` 📖	CompOp	2 math math: `mk''_rightQuotientEquiv`, `rightQuotientEquiv_apply`
`toLeftFun` 📖	CompOp	3 math math: `neg_toLeftFun_add_mem`, `neg_add_toLeftFun_mem`, `AddSubgroup.vadd_toLeftFun`
`toRightFun` 📖	CompOp	2 math math: `toRightFun_add_neg_mem`, `add_neg_toRightFun_mem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_eq` 📖	mathematical	`AddSubgroup.IsComplement`	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Set.univ`	—	`Set.eq_univ_of_forall` `Set.mem_add` `ExistsUnique.exists` `existsUnique`
`add_neg_toRightFun_mem` 📖	mathematical	`AddSubgroup.IsComplement` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	`SetLike.instMembership` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Set` `Set.instMembership` `toRightFun`	—	`QuotientAddGroup.rightRel_apply` `Quotient.exact'` `mk''_rightQuotientEquiv`
`card_left` 📖	mathematical	`AddSubgroup.IsComplement` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	`Nat.card` `Set.Elem` `AddSubgroup.index`	—	`Nat.card_congr` `AddSubgroup.isComplement_addSubgroup_right_iff_bijective`
`card_mul_card` 📖	mathematical	`AddSubgroup.IsComplement`	`Nat.card` `Set.Elem`	—	`Nat.card_prod` `Nat.card_congr`
`card_right` 📖	mathematical	`AddSubgroup.IsComplement` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	`Nat.card` `Set.Elem` `AddSubgroup.index`	—	`Nat.card_congr` `AddSubgroup.isComplement_addSubgroup_left_iff_bijective`
`encard_left` 📖	mathematical	`AddSubgroup.IsComplement` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	`Set.encard` `ENat` `ENat.instNatCast` `AddSubgroup.index`	—	`Set.Finite.cast_ncard_eq` `finite_left` `ncard_left`
`encard_right` 📖	mathematical	`AddSubgroup.IsComplement` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	`Set.encard` `ENat` `ENat.instNatCast` `AddSubgroup.index`	—	`Set.Finite.cast_ncard_eq` `finite_right` `ncard_right`
`existsUnique` 📖	mathematical	`AddSubgroup.IsComplement`	`ExistsUnique` `Set.Elem` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Set` `Set.instMembership`	—	`AddSubgroup.isComplement_iff_existsUnique`
`finite_left` 📖	mathematical	`AddSubgroup.IsComplement` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	`Set.Finite`	—	`finite_left_iff`
`finite_left_iff` 📖	mathematical	`AddSubgroup.IsComplement` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	`Finite` `Set.Elem` `AddSubgroup.FiniteIndex`	—	`Equiv.finite_iff` `AddSubgroup.finiteIndex_of_finite_quotient` `AddSubgroup.finite_quotient_of_finiteIndex`
`finite_right` 📖	mathematical	`AddSubgroup.IsComplement` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	`Set.Finite`	—	`finite_right_iff`
`finite_right_iff` 📖	mathematical	`AddSubgroup.IsComplement` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	`Finite` `Set.Elem` `AddSubgroup.FiniteIndex`	—	`Equiv.finite_iff` `AddSubgroup.finiteIndex_of_finite_quotient` `AddSubgroup.finite_quotient_of_finiteIndex`
`leftQuotientEquiv_apply` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `HasQuotient.Quotient` `AddSubgroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `leftQuotientEquiv` `AddSubgroup.isComplement_range_left`	—	`AddSubgroup.isComplement_range_left` `Equiv.apply_eq_iff_eq_symm_apply`
`mk''_rightQuotientEquiv` 📖	mathematical	`AddSubgroup.IsComplement` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	`Quotient.mk''` `QuotientAddGroup.rightRel` `Set` `Set.instMembership` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `rightQuotientEquiv`	—	`Equiv.symm_apply_apply`
`ncard_left` 📖	mathematical	`AddSubgroup.IsComplement` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	`Set.ncard` `AddSubgroup.index`	—	`Nat.card_coe_set_eq` `card_left`
`ncard_right` 📖	mathematical	`AddSubgroup.IsComplement` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	`Set.ncard` `AddSubgroup.index`	—	`Nat.card_coe_set_eq` `card_right`
`neg_add_toLeftFun_mem` 📖	mathematical	`AddSubgroup.IsComplement` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	`SetLike.instMembership` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Set` `Set.instMembership` `toLeftFun`	—	`neg_add_rev` `neg_neg` `AddSubgroup.neg_mem` `neg_toLeftFun_add_mem`
`neg_toLeftFun_add_mem` 📖	mathematical	`AddSubgroup.IsComplement` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	`SetLike.instMembership` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Set` `Set.instMembership` `toLeftFun`	—	`QuotientAddGroup.leftRel_apply` `Quotient.exact'` `quotientAddGroupMk_leftQuotientEquiv`
`nonempty_left` 📖	mathematical	`AddSubgroup.IsComplement`	`Set.Nonempty`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Set.not_nonempty_iff_eq_empty` `AddSubgroup.not_isComplement_empty_left`
`nonempty_right` 📖	mathematical	`AddSubgroup.IsComplement`	`Set.Nonempty`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Set.not_nonempty_iff_eq_empty` `AddSubgroup.not_isComplement_empty_right`
`pairwiseDisjoint_vadd` 📖	mathematical	`AddSubgroup.IsComplement`	`Set.PairwiseDisjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction`	—	`Set.disjoint_iff_forall_ne`
`quotientAddGroupMk_leftQuotientEquiv` 📖	mathematical	`AddSubgroup.IsComplement` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	`Quotient.mk''` `QuotientAddGroup.leftRel` `Set` `Set.instMembership` `DFunLike.coe` `Equiv` `HasQuotient.Quotient` `QuotientAddGroup.instHasQuotientAddSubgroup` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `leftQuotientEquiv`	—	`Equiv.symm_apply_apply`
`rightQuotientEquiv_apply` 📖	mathematical	`Quotient.mk''` `QuotientAddGroup.rightRel`	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `rightQuotientEquiv` `AddSubgroup.isComplement_range_right`	—	`AddSubgroup.isComplement_range_right` `Equiv.apply_eq_iff_eq_symm_apply`
`toRightFun_add_neg_mem` 📖	mathematical	`AddSubgroup.IsComplement` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	`SetLike.instMembership` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Set` `Set.instMembership` `toRightFun` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`neg_add_rev` `neg_neg` `AddSubgroup.neg_mem` `add_neg_toRightFun_mem`

Subgroup

Definitions

Name	Category	Theorems
`IsComplement` 📖	MathDef	30 math math: `isComplement_singleton_univ`, `isComplement_singleton_right`, `transferTransversal_apply`, `not_isComplement_empty_right`, `Monoid.PushoutI.NormalWord.Transversal.compl`, `isComplement_range_right`, `smul_leftQuotientEquiv`, `isComplement_iff_bijective`, `isComplement_subgroup_left_iff_existsUnique_quotientMk''`, `smul_apply_eq_smul_apply_inv_smul`, `isComplement_iff_existsUnique`, `exists_leftTransversal_of_FiniteIndex`, `exists_isComplement_left`, `isComplement_singleton_left`, `transferTransversal_apply'`, `isComplement_range_left`, `isComplement_subgroup_left_iff_bijective`, `isComplement_iff_existsUnique_inv_mul_mem`, `not_isComplement_empty_left`, `isComplement_iff_existsUnique_mul_inv_mem`, `HNNExtension.NormalWord.TransversalPair.compl`, `transferTransversal_apply''`, `isComplement_subgroup_right_iff_existsUnique_quotientGroupMk`, `smul_toLeftFun`, `isComplement_univ_singleton`, `exists_isComplement_right`, `isComplement_univ_right`, `isComplement_subgroup_right_iff_bijective`, `isComplement'_def`, `isComplement_univ_left`
`IsComplement'` 📖	MathDef	18 math math: `isComplement'_top_left`, `IsCyclic.isComplement'`, `MonoidHom.ker_transferSylow_isComplement'`, `isComplement'_of_disjoint_and_mul_eq_univ`, `isComplement'_bot_right`, `isComplement'_stabilizer`, `isComplement'_top_right`, `isComplement'_comm`, `exists_right_complement'_of_coprime`, `exists_left_complement'_of_coprime`, `isComplement'_bot_left`, `isComplement'_stabilizer_of_coprime`, `isComplement'_of_card_mul_and_disjoint`, `isComplement'_top_bot`, `isComplement'_of_coprime`, `isComplement'_iff_card_mul_and_disjoint`, `isComplement'_bot_top`, `isComplement'_def`
`LeftTransversal` 📖	CompOp	8 math math: `smul_leftQuotientEquiv`, `smul_diff_smul'`, `MonoidHom.transfer_def`, `leftTransversals.smul_diff_smul`, `smul_apply_eq_smul_apply_inv_smul`, `transferTransversal_apply''`, `smul_toLeftFun`, `smul_diff'`
`RightTransversal` 📖	CompOp	—
`instInhabitedLeftTransversal` 📖	CompOp	—
`instInhabitedRightTransversal` 📖	CompOp	—
`instMulActionLeftTransversal` 📖	CompOp	8 math math: `smul_leftQuotientEquiv`, `smul_diff_smul'`, `MonoidHom.transfer_def`, `leftTransversals.smul_diff_smul`, `smul_apply_eq_smul_apply_inv_smul`, `transferTransversal_apply''`, `smul_toLeftFun`, `smul_diff'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isComplement_left` 📖	mathematical	—	`IsComplement` `SetLike.coe` `Subgroup` `instSetLike` `Set` `Set.instMembership`	—	`isComplement_range_left` `Function.update_self` `Quotient.out_eq'`
`exists_isComplement_right` 📖	mathematical	—	`IsComplement` `SetLike.coe` `Subgroup` `instSetLike` `Set` `Set.instMembership`	—	`isComplement_range_right` `Function.update_self` `Quotient.out_eq'`
`exists_left_transversal_of_le` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `instSetLike` `Nat.card` `Set.Elem` `SetLike.instMembership`	—	`subgroupOf_map_subtype` `inf_of_le_left` `exists_isComplement_left` `Set.image_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `IsComplement.mul_eq` `Set.image_congr` `Set.image_univ` `Subtype.range_coe_subtype` `IsComplement.card_mul_card` `Nat.card_congr` `subtype_injective`
`exists_right_transversal_of_le` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `instSetLike` `Nat.card` `SetLike.instMembership` `Set.Elem`	—	`subgroupOf_map_subtype` `inf_of_le_left` `exists_isComplement_right` `Set.image_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `IsComplement.mul_eq` `Set.image_congr` `Set.image_univ` `Subtype.range_coe_subtype` `IsComplement.card_mul_card` `Nat.card_congr` `subtype_injective`
`isComplement'_bot_left` 📖	mathematical	—	`IsComplement'` `Bot.bot` `Subgroup` `instBot` `Top.top` `instTop`	—	`isComplement_singleton_left` `coe_eq_univ`
`isComplement'_bot_right` 📖	mathematical	—	`IsComplement'` `Bot.bot` `Subgroup` `instBot` `Top.top` `instTop`	—	`isComplement_singleton_right` `coe_eq_univ`
`isComplement'_bot_top` 📖	mathematical	—	`IsComplement'` `Bot.bot` `Subgroup` `instBot` `Top.top` `instTop`	—	`isComplement_singleton_univ`
`isComplement'_comm` 📖	mathematical	—	`IsComplement'`	—	`IsComplement'.symm`
`isComplement'_def` 📖	mathematical	—	`IsComplement'` `IsComplement` `SetLike.coe` `Subgroup` `instSetLike`	—	—
`isComplement'_iff_card_mul_and_disjoint` 📖	mathematical	—	`IsComplement'` `Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike` `Disjoint` `instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `instCompleteLattice`	—	`IsComplement'.card_mul` `IsComplement'.disjoint` `isComplement'_of_card_mul_and_disjoint`
`isComplement'_of_card_mul_and_disjoint` 📖	mathematical	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike` `Disjoint` `instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `instCompleteLattice`	`IsComplement'`	—	`Nat.bijective_iff_injective_and_card` `mul_injective_of_disjoint` `Nat.card_prod`
`isComplement'_of_coprime` 📖	mathematical	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike`	`IsComplement'`	—	`isComplement'_of_card_mul_and_disjoint` `disjoint_iff` `inf_eq_bot_of_coprime`
`isComplement'_of_disjoint_and_mul_eq_univ` 📖	mathematical	`Disjoint` `Subgroup` `instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `instCompleteLattice` `Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `instSetLike` `Set.univ`	`IsComplement'`	—	`mul_injective_of_disjoint` `Set.eq_univ_iff_forall`
`isComplement'_stabilizer` 📖	mathematical	`Subgroup` `SetLike.instMembership` `instSetLike` `one` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `MulAction.toSemigroupAction` `instMulAction`	`IsComplement'` `MulAction.stabilizer`	—	`isComplement_iff_existsUnique` `SemigroupAction.mul_smul` `SubgroupClass.toInvMemClass` `instSubgroupClass` `inv_mul_cancel_left` `eq_inv_of_mul_eq_one_right` `SubmonoidClass.toMulMemClass` `SubgroupClass.toSubmonoidClass` `smul_def` `mul_assoc` `right_eq_mul` `RightCancelSemigroup.toIsRightCancelMul` `coe_mul` `coe_one`
`isComplement'_top_bot` 📖	mathematical	—	`IsComplement'` `Top.top` `Subgroup` `instTop` `Bot.bot` `instBot`	—	`isComplement_univ_singleton`
`isComplement'_top_left` 📖	mathematical	—	`IsComplement'` `Top.top` `Subgroup` `instTop` `Bot.bot` `instBot`	—	`isComplement_univ_left` `coe_eq_singleton`
`isComplement'_top_right` 📖	mathematical	—	`IsComplement'` `Top.top` `Subgroup` `instTop` `Bot.bot` `instBot`	—	`isComplement_univ_right` `coe_eq_singleton`
`isComplement_iff_bijective` 📖	mathematical	—	`IsComplement` `SetLike.coe` `Function.Bijective` `SetLike.instMembership` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`isComplement_iff_existsUnique` 📖	mathematical	—	`IsComplement` `ExistsUnique` `Set.Elem` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set` `Set.instMembership`	—	`Function.bijective_iff_existsUnique`
`isComplement_iff_existsUnique_inv_mul_mem` 📖	mathematical	—	`IsComplement` `ExistsUnique` `Set.Elem` `Set` `Set.instMembership` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`mul_inv_cancel_left` `inv_mul_cancel_left` `isComplement_iff_existsUnique`
`isComplement_iff_existsUnique_mul_inv_mem` 📖	mathematical	—	`IsComplement` `ExistsUnique` `Set.Elem` `Set` `Set.instMembership` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`inv_mul_cancel_right` `mul_inv_cancel_right` `isComplement_iff_existsUnique`
`isComplement_range_left` 📖	mathematical	—	`IsComplement` `Set.range` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `SetLike.coe` `instSetLike`	—	`isComplement_subgroup_right_iff_bijective`
`isComplement_range_right` 📖	mathematical	`Quotient.mk''` `QuotientGroup.rightRel`	`IsComplement` `SetLike.coe` `Subgroup` `instSetLike` `Set.range`	—	`isComplement_subgroup_left_iff_bijective`
`isComplement_singleton_left` 📖	mathematical	—	`IsComplement` `Set` `Set.instSingletonSet` `Set.univ`	—	`top_le_iff` `mul_left_cancel` `LeftCancelSemigroup.toIsLeftCancelMul` `isComplement_singleton_univ`
`isComplement_singleton_right` 📖	mathematical	—	`IsComplement` `Set` `Set.instSingletonSet` `Set.univ`	—	`top_le_iff` `mul_right_cancel` `RightCancelSemigroup.toIsRightCancelMul` `isComplement_univ_singleton`
`isComplement_singleton_univ` 📖	mathematical	—	`IsComplement` `Set` `Set.instSingletonSet` `Set.univ`	—	`mul_left_cancel` `LeftCancelSemigroup.toIsLeftCancelMul` `mul_inv_cancel_left`
`isComplement_subgroup_left_iff_bijective` 📖	mathematical	—	`IsComplement` `SetLike.coe` `Subgroup` `instSetLike` `Function.Bijective` `Set.Elem` `QuotientGroup.rightRel` `Set.restrict` `Quotient.mk''`	—	`isComplement_subgroup_left_iff_existsUnique_quotientMk''` `Function.bijective_iff_existsUnique`
`isComplement_subgroup_left_iff_existsUnique_quotientMk''` 📖	mathematical	—	`IsComplement` `SetLike.coe` `Subgroup` `instSetLike` `ExistsUnique` `Set.Elem` `QuotientGroup.rightRel` `Quotient.mk''` `Set` `Set.instMembership`	—	—
`isComplement_subgroup_right_iff_bijective` 📖	mathematical	—	`IsComplement` `SetLike.coe` `Subgroup` `instSetLike` `Function.Bijective` `Set.Elem` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup` `Set.restrict`	—	`isComplement_subgroup_right_iff_existsUnique_quotientGroupMk` `Function.bijective_iff_existsUnique`
`isComplement_subgroup_right_iff_existsUnique_quotientGroupMk` 📖	mathematical	—	`IsComplement` `SetLike.coe` `Subgroup` `instSetLike` `ExistsUnique` `Set.Elem` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup` `Set` `Set.instMembership`	—	—
`isComplement_univ_left` 📖	mathematical	—	`IsComplement` `Set.univ` `Set` `Set.instSingletonSet`	—	`Set.exists_eq_singleton_iff_nonempty_subsingleton` `mem_top` `inv_mul_cancel` `isComplement_univ_singleton`
`isComplement_univ_right` 📖	mathematical	—	`IsComplement` `Set.univ` `Set` `Set.instSingletonSet`	—	`Set.exists_eq_singleton_iff_nonempty_subsingleton` `mem_top` `mul_inv_cancel` `isComplement_singleton_univ`
`isComplement_univ_singleton` 📖	mathematical	—	`IsComplement` `Set.univ` `Set` `Set.instSingletonSet`	—	`mul_right_cancel` `RightCancelSemigroup.toIsRightCancelMul` `inv_mul_cancel_right`
`not_isComplement_empty_left` 📖	mathematical	—	`IsComplement` `Set` `Set.instEmptyCollection`	—	`Set.empty_mul` `One.instNonempty` `IsComplement.mul_eq`
`not_isComplement_empty_right` 📖	mathematical	—	`IsComplement` `Set` `Set.instEmptyCollection`	—	`Set.mul_empty` `One.instNonempty` `IsComplement.mul_eq`
`smul_apply_eq_smul_apply_inv_smul` 📖	mathematical	—	`Set` `Set.instMembership` `IsComplement` `SetLike.coe` `Subgroup` `instSetLike` `LeftTransversal` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `instMulActionLeftTransversal` `DFunLike.coe` `Equiv` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `IsComplement.leftQuotientEquiv` `MulAction.quotient` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`smul_leftQuotientEquiv` `smul_inv_smul`
`smul_leftQuotientEquiv` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set` `Set.instMembership` `IsComplement` `SetLike.coe` `Subgroup` `instSetLike` `DFunLike.coe` `Equiv` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `IsComplement.leftQuotientEquiv` `LeftTransversal` `instMulActionLeftTransversal` `MulAction.quotient`	—	`Quotient.inductionOn'` `smul_toLeftFun`
`smul_toLeftFun` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set` `Set.instMembership` `IsComplement` `SetLike.coe` `Subgroup` `instSetLike` `IsComplement.toLeftFun` `LeftTransversal` `instMulActionLeftTransversal`	—	`Set.smul_mem_smul_set` `Subtype.coe_prop` `ExistsUnique.unique` `isComplement_iff_existsUnique_inv_mul_mem` `MulAction.QuotientAction.inv_mul_mem` `IsComplement.inv_toLeftFun_mul_mem`

Subgroup.IsComplement

Definitions

Name	Category	Theorems
`equiv` 📖	CompOp	24 math math: `equiv_fst_eq_iff_leftCosetEquivalence`, `coe_equiv_snd_eq_one_iff_mem`, `equiv_snd_eq_self_iff_mem`, `equiv_one`, `equiv_mul_left_of_mem`, `equiv_snd_eq_iff_rightCosetEquivalence`, `leftCosetEquivalence_equiv_fst`, `Monoid.PushoutI.NormalWord.cons_head`, `equiv_fst_eq_self_of_mem_of_one_mem`, `equiv_fst_eq_one_of_mem_of_one_mem`, `HNNExtension.NormalWord.unitsSMulGroup_snd`, `equiv_snd_eq_self_of_mem_of_one_mem`, `equiv_snd_eq_one_of_mem_of_one_mem`, `equiv_fst_mul_equiv_snd`, `equiv_symm_apply`, `rightCosetEquivalence_equiv_snd`, `coe_equiv_fst_eq_one_iff_mem`, `equiv_mul_right_of_mem`, `equiv_mul_right`, `equiv_fst_eq_mul_inv`, `equiv_mul_left`, `equiv_snd_eq_inv_mul`, `equiv_fst_eq_self_iff_mem`, `Monoid.PushoutI.NormalWord.cons_toList`
`leftQuotientEquiv` 📖	CompOp	9 math math: `Subgroup.transferTransversal_apply`, `Subgroup.smul_leftQuotientEquiv`, `Subgroup.smul_apply_eq_smul_apply_inv_smul`, `Subgroup.transferTransversal_apply'`, `Subgroup.IsComplement'.QuotientMulEquiv_symm_apply`, `Subgroup.transferTransversal_apply''`, `Subgroup.IsComplement'.QuotientMulEquiv_apply`, `leftQuotientEquiv_apply`, `quotientGroupMk_leftQuotientEquiv`
`rightQuotientEquiv` 📖	CompOp	2 math math: `mk''_rightQuotientEquiv`, `rightQuotientEquiv_apply`
`toLeftFun` 📖	CompOp	3 math math: `inv_mul_toLeftFun_mem`, `inv_toLeftFun_mul_mem`, `Subgroup.smul_toLeftFun`
`toRightFun` 📖	CompOp	6 math math: `mul_inv_toRightFun_mem`, `Subgroup.closure_mul_image_eq`, `Subgroup.closure_mul_image_mul_eq_top`, `Subgroup.closure_mul_image_eq_top`, `toRightFun_mul_inv_mem`, `Subgroup.closure_mul_image_eq_top'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_left` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`Nat.card` `Set.Elem` `Subgroup.index`	—	`Nat.card_congr` `Subgroup.isComplement_subgroup_right_iff_bijective`
`card_mul` 📖	mathematical	`Subgroup.IsComplement`	`Nat.card` `Set.Elem`	—	`Nat.card_prod` `Nat.card_eq_of_bijective`
`card_mul_card` 📖	mathematical	`Subgroup.IsComplement`	`Nat.card` `Set.Elem`	—	`Nat.card_prod` `Nat.card_congr`
`card_right` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`Nat.card` `Set.Elem` `Subgroup.index`	—	`Nat.card_congr` `Subgroup.isComplement_subgroup_left_iff_bijective`
`coe_equiv_fst_eq_one_iff_mem` 📖	mathematical	`Subgroup.IsComplement` `Set` `Set.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`Set.Elem` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv`	—	`equiv_fst_eq_mul_inv` `mul_inv_eq_one` `equiv_snd_eq_self_iff_mem`
`coe_equiv_snd_eq_one_iff_mem` 📖	mathematical	`Subgroup.IsComplement` `Set` `Set.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`Set.Elem` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv`	—	`equiv_snd_eq_inv_mul` `inv_mul_eq_one` `equiv_fst_eq_self_iff_mem`
`encard_left` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`Set.encard` `ENat` `ENat.instNatCast` `Subgroup.index`	—	`Set.Finite.cast_ncard_eq` `finite_left` `ncard_left`
`encard_right` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`Set.encard` `ENat` `ENat.instNatCast` `Subgroup.index`	—	`Set.Finite.cast_ncard_eq` `finite_right` `ncard_right`
`equiv_fst_eq_iff_leftCosetEquivalence` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`Set.Elem` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `LeftCosetEquivalence` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`LeftCosetEquivalence.eq_1` `leftCoset_eq_iff` `equiv_fst_mul_equiv_snd` `mul_inv_rev` `mul_assoc` `inv_mul_cancel_right` `Subgroup.coe_inv` `Subgroup.coe_mul` `ExistsUnique.unique` `Subgroup.isComplement_iff_existsUnique_inv_mul_mem` `equiv_fst_eq_mul_inv` `inv_inv` `SetLike.mem_coe` `mul_mem_cancel_right` `Subgroup.instSubgroupClass` `mul_inv_cancel_right`
`equiv_fst_eq_mul_inv` 📖	mathematical	`Subgroup.IsComplement`	`Set` `Set.instMembership` `Set.Elem` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`eq_mul_inv_of_mul_eq` `equiv_fst_mul_equiv_snd`
`equiv_fst_eq_one_of_mem_of_one_mem` 📖	mathematical	`Subgroup.IsComplement` `Set` `Set.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`Set.Elem` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv`	—	`equiv_fst_eq_mul_inv` `equiv_snd_eq_self_of_mem_of_one_mem` `mul_inv_cancel`
`equiv_fst_eq_self_iff_mem` 📖	mathematical	`Subgroup.IsComplement` `Set` `Set.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`Set.Elem` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv`	—	`Subtype.prop` `equiv_fst_eq_self_of_mem_of_one_mem`
`equiv_fst_eq_self_of_mem_of_one_mem` 📖	mathematical	`Subgroup.IsComplement` `Set` `Set.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`Set.Elem` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv`	—	`equiv.eq_1` `Function.Bijective.surjective` `Function.leftInverse_surjInv` `Equiv.ofBijective.eq_1` `mul_one` `Equiv.apply_symm_apply`
`equiv_fst_mul_equiv_snd` 📖	mathematical	`Subgroup.IsComplement`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set` `Set.instMembership` `Set.Elem` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv`	—	`Equiv.right_inv`
`equiv_mul_left` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.instMembership` `Subgroup.mul`	—	`equiv_snd_eq_iff_rightCosetEquivalence` `op_smul_coe_set` `Subgroup.instSubgroupClass` `Subgroup.coe_mul` `equiv_fst_eq_mul_inv` `mul_assoc`
`equiv_mul_left_of_mem` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `SetLike.instMembership`	`DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SubgroupClass.toGroup` `Subgroup.instSubgroupClass` `Set` `Set.instMembership`	—	`equiv_mul_left`
`equiv_mul_right` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.instMembership` `SubgroupClass.toGroup` `Subgroup.instSubgroupClass`	—	`equiv_fst_eq_iff_leftCosetEquivalence` `mul_inv_rev` `inv_mul_cancel_right` `SubgroupClass.toInvMemClass` `Subgroup.instSubgroupClass` `Subgroup.coe_mul` `equiv_snd_eq_inv_mul` `mul_assoc`
`equiv_mul_right_of_mem` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `SetLike.instMembership`	`DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SubgroupClass.toGroup` `Subgroup.instSubgroupClass` `Set` `Set.instMembership`	—	`equiv_mul_right`
`equiv_one` 📖	mathematical	`Subgroup.IsComplement` `Set` `Set.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv`	—	`Equiv.apply_eq_iff_eq_symm_apply` `mul_one`
`equiv_snd_eq_iff_rightCosetEquivalence` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`Set.Elem` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `RightCosetEquivalence` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`RightCosetEquivalence.eq_1` `rightCoset_eq_iff` `equiv_fst_mul_equiv_snd` `mul_inv_rev` `mul_assoc` `mul_inv_cancel_left` `Subgroup.coe_inv` `Subgroup.coe_mul` `ExistsUnique.unique` `Subgroup.isComplement_iff_existsUnique_mul_inv_mem` `equiv_snd_eq_inv_mul` `inv_inv` `SetLike.mem_coe` `mul_mem_cancel_left` `Subgroup.instSubgroupClass` `inv_mul_cancel_left`
`equiv_snd_eq_inv_mul` 📖	mathematical	`Subgroup.IsComplement`	`Set` `Set.instMembership` `Set.Elem` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`eq_inv_mul_of_mul_eq` `equiv_fst_mul_equiv_snd`
`equiv_snd_eq_one_of_mem_of_one_mem` 📖	mathematical	`Subgroup.IsComplement` `Set` `Set.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`Set.Elem` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv`	—	`equiv_snd_eq_inv_mul` `equiv_fst_eq_self_of_mem_of_one_mem` `inv_mul_cancel`
`equiv_snd_eq_self_iff_mem` 📖	mathematical	`Subgroup.IsComplement` `Set` `Set.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`Set.Elem` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv`	—	`Subtype.prop` `equiv_snd_eq_self_of_mem_of_one_mem`
`equiv_snd_eq_self_of_mem_of_one_mem` 📖	mathematical	`Subgroup.IsComplement` `Set` `Set.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`Set.Elem` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv`	—	`equiv.eq_1` `Function.Bijective.surjective` `Function.leftInverse_surjInv` `Equiv.ofBijective.eq_1` `one_mul` `Equiv.apply_symm_apply`
`equiv_symm_apply` 📖	mathematical	`Subgroup.IsComplement`	`DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set` `Set.instMembership`	—	—
`existsUnique` 📖	mathematical	`Subgroup.IsComplement`	`ExistsUnique` `Set.Elem` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set` `Set.instMembership`	—	`Subgroup.isComplement_iff_existsUnique`
`finite_left` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`Set.Finite`	—	`finite_left_iff`
`finite_left_iff` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`Finite` `Set.Elem` `Subgroup.FiniteIndex`	—	`Equiv.finite_iff` `Subgroup.finiteIndex_of_finite_quotient` `Subgroup.finite_quotient_of_finiteIndex`
`finite_right` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`Set.Finite`	—	`finite_right_iff`
`finite_right_iff` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`Finite` `Set.Elem` `Subgroup.FiniteIndex`	—	`Equiv.finite_iff` `Subgroup.finiteIndex_of_finite_quotient` `Subgroup.finite_quotient_of_finiteIndex`
`inv_mul_toLeftFun_mem` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`SetLike.instMembership` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Set` `Set.instMembership` `toLeftFun`	—	`mul_inv_rev` `inv_inv` `Subgroup.inv_mem` `inv_toLeftFun_mul_mem`
`inv_toLeftFun_mul_mem` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`SetLike.instMembership` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Set` `Set.instMembership` `toLeftFun`	—	`QuotientGroup.leftRel_apply` `Quotient.exact'` `quotientGroupMk_leftQuotientEquiv`
`leftCosetEquivalence_equiv_fst` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`LeftCosetEquivalence` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set` `Set.instMembership` `Set.Elem` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv`	—	`equiv_fst_eq_mul_inv` `inv_mul_cancel_left` `SubgroupClass.toInvMemClass` `Subgroup.instSubgroupClass`
`leftQuotientEquiv_apply` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `leftQuotientEquiv` `Subgroup.isComplement_range_left`	—	`Subgroup.isComplement_range_left` `Equiv.apply_eq_iff_eq_symm_apply`
`mk''_rightQuotientEquiv` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`Quotient.mk''` `QuotientGroup.rightRel` `Set` `Set.instMembership` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `rightQuotientEquiv`	—	`Equiv.symm_apply_apply`
`mul_eq` 📖	mathematical	`Subgroup.IsComplement`	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set.univ`	—	`Set.eq_univ_of_forall` `ExistsUnique.exists` `existsUnique`
`mul_inv_toRightFun_mem` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`SetLike.instMembership` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Set` `Set.instMembership` `toRightFun`	—	`QuotientGroup.rightRel_apply` `Quotient.exact'` `mk''_rightQuotientEquiv`
`ncard_left` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`Set.ncard` `Subgroup.index`	—	`Nat.card_coe_set_eq` `card_left`
`ncard_right` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`Set.ncard` `Subgroup.index`	—	`Nat.card_coe_set_eq` `card_right`
`nonempty_left` 📖	mathematical	`Subgroup.IsComplement`	`Set.Nonempty`	—	`Mathlib.Tactic.Contrapose.contrapose₁`
`nonempty_right` 📖	mathematical	`Subgroup.IsComplement`	`Set.Nonempty`	—	`Mathlib.Tactic.Contrapose.contrapose₁`
`pairwiseDisjoint_smul` 📖	mathematical	`Subgroup.IsComplement`	`Set.PairwiseDisjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction`	—	`Set.disjoint_iff_forall_ne`
`quotientGroupMk_leftQuotientEquiv` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`Quotient.mk''` `QuotientGroup.leftRel` `Set` `Set.instMembership` `DFunLike.coe` `Equiv` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `leftQuotientEquiv`	—	`Equiv.symm_apply_apply`
`rightCosetEquivalence_equiv_snd` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`RightCosetEquivalence` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set` `Set.instMembership` `Set.Elem` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv`	—	`RightCosetEquivalence.eq_1` `rightCoset_eq_iff` `equiv_snd_eq_inv_mul` `mul_inv_cancel_right` `SubgroupClass.toInvMemClass` `Subgroup.instSubgroupClass`
`rightQuotientEquiv_apply` 📖	mathematical	`Quotient.mk''` `QuotientGroup.rightRel`	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `rightQuotientEquiv` `Subgroup.isComplement_range_right`	—	`Subgroup.isComplement_range_right` `Equiv.apply_eq_iff_eq_symm_apply`
`toRightFun_mul_inv_mem` 📖	mathematical	`Subgroup.IsComplement` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`SetLike.instMembership` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set` `Set.instMembership` `toRightFun` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`mul_inv_rev` `inv_inv` `Subgroup.inv_mem` `mul_inv_toRightFun_mem`

Subgroup.IsComplement'

Definitions

Name	Category	Theorems
`QuotientMulEquiv` 📖	CompOp	2 math math: `QuotientMulEquiv_symm_apply`, `QuotientMulEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`QuotientMulEquiv_apply` 📖	mathematical	`Subgroup.IsComplement'`	`DFunLike.coe` `MulEquiv` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `QuotientGroup.Quotient.group` `Subgroup.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `QuotientMulEquiv` `Equiv` `Equiv.instEquivLike` `Subgroup.IsComplement.leftQuotientEquiv` `SetLike.coe`	—	—
`QuotientMulEquiv_symm_apply` 📖	mathematical	`Subgroup.IsComplement'`	`DFunLike.coe` `MulEquiv` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup` `Subgroup.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `QuotientGroup.Quotient.group` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `QuotientMulEquiv` `Equiv` `Equiv.instEquivLike` `Equiv.symm` `Subgroup.IsComplement.leftQuotientEquiv` `SetLike.coe`	—	—
`card_mul` 📖	mathematical	`Subgroup.IsComplement'`	`Nat.card` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike`	—	`Subgroup.IsComplement.card_mul`
`disjoint` 📖	mathematical	`Subgroup.IsComplement'`	`Disjoint` `Subgroup` `Subgroup.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Subgroup.instCompleteLattice`	—	`IsCompl.disjoint` `isCompl`
`index_eq_card` 📖	mathematical	`Subgroup.IsComplement'`	`Subgroup.index` `Nat.card` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike`	—	`Subgroup.IsComplement.card_left`
`isCompl` 📖	mathematical	`Subgroup.IsComplement'`	`IsCompl` `Subgroup` `Subgroup.instPartialOrder` `CompleteLattice.toBoundedOrder` `Subgroup.instCompleteLattice`	—	`disjoint_iff_inf_le` `mul_one` `one_mul` `codisjoint_iff_le_sup` `Subgroup.mul_mem_sup`
`sup_eq_top` 📖	mathematical	`Subgroup.IsComplement'`	`Subgroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Subgroup.instCompleteLattice` `Top.top` `Subgroup.instTop`	—	`IsCompl.sup_eq_top` `isCompl`

---

← Back to Index