Documentation Verification Report

Transfer

📁 Source: Mathlib/GroupTheory/Transfer.lean

Statistics

Metric	Count
Definitions `transfer`, `diff`, `transfer`, `transferCenterPow`, `transferSylow`, `diff`, `transferFunction`, `transferSet`, `transferTransversal`	9
Theorems `transfer_def`, `diff_add_diff`, `diff_neg`, `diff_self`, `vadd_diff_vadd`, `isComplement'`, `normalizer_le_centralizer`, `ker_transferSylow_disjoint`, `ker_transferSylow_isComplement'`, `not_dvd_card_ker_transferSylow`, `transferCenterPow_apply`, `transferSylow_eq_pow`, `transferSylow_eq_pow_aux`, `transferSylow_restrict_eq_pow`, `transfer_center_eq_pow`, `transfer_def`, `transfer_eq_pow`, `transfer_eq_pow_aux`, `transfer_eq_prod_quotient_orbitRel_zpowers_quot`, `coe_transferFunction`, `diff_inv`, `diff_mul_diff`, `diff_self`, `smul_diff_smul`, `mem_transferSet`, `transferFunction_apply`, `transferTransversal_apply`, `transferTransversal_apply'`, `transferTransversal_apply''`	29
Total	38

AddMonoidHom

Definitions

Name	Category	Theorems
`transfer` 📖	CompOp	1 math math: `transfer_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`transfer_def` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instFunLike` `transfer` `AddSubgroup.leftTransversals.diff` `HVAdd.hVAdd` `AddSubgroup.LeftTransversal` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddSubgroup.instAddActionLeftTransversal` `AddMonoid.toAddAction` `AddAction.left_quotientAction`	—	`AddAction.left_quotientAction` `transfer.eq_1` `AddSubgroup.leftTransversals.diff_add_diff` `AddSubgroup.leftTransversals.vadd_diff_vadd` `add_comm`

AddSubgroup.leftTransversals

Definitions

Name	Category	Theorems
`diff` 📖	CompOp	5 math math: `diff_add_diff`, `vadd_diff_vadd`, `diff_neg`, `AddMonoidHom.transfer_def`, `diff_self`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diff_add_diff` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `diff`	—	`Finset.sum_add_distrib` `Finset.sum_congr` `AddMonoidHom.map_add` `add_assoc` `add_neg_cancel_left`
`diff_neg` 📖	mathematical	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `diff`	—	`neg_eq_of_add_eq_zero_right` `diff_add_diff` `diff_self`
`diff_self` 📖	mathematical	—	`diff` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`add_eq_left` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `diff_add_diff`
`vadd_diff_vadd` 📖	mathematical	—	`diff` `HVAdd.hVAdd` `AddSubgroup.LeftTransversal` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddSubgroup.instAddActionLeftTransversal` `AddMonoid.toAddAction` `AddAction.left_quotientAction`	—	`Fintype.sum_equiv` `AddAction.left_quotientAction` `AddSubgroup.vadd_apply_eq_vadd_apply_neg_vadd` `neg_add_rev` `add_assoc` `neg_add_cancel_left`

IsCyclic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isComplement'` 📖	mathematical	`Nat.minFac` `Nat.card`	`Subgroup.IsComplement'` `MonoidHom.ker` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Sylow.toSubgroup` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MonoidHom.transferSylow` `normalizer_le_centralizer` `Subgroup.finiteIndex_of_finite`	—	`normalizer_le_centralizer` `Subgroup.finiteIndex_of_finite` `Nat.card_eq_one_iff_unique` `Unique.instSubsingleton` `Subgroup.isComplement'_bot_top` `Nat.minFac_prime` `MonoidHom.ker_transferSylow_isComplement'` `SetLike.instFinite`
`normalizer_le_centralizer` 📖	mathematical	`Nat.minFac` `Nat.card`	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.normalizer` `Sylow.toSubgroup` `Subgroup.centralizer` `SetLike.coe` `Sylow` `Sylow.instSetLike`	—	`Nat.card_eq_one_iff_unique` `Unique.instSubsingleton` `le_refl` `Nat.minFac_prime` `Subgroup.card_dvd_of_injective` `MonoidHom.normal_ker` `QuotientGroup.kerLift_injective` `Subgroup.relIndex_eq_one` `Nat.eq_one_of_dvd_coprimes` `IsPGroup.exists_card_eq` `Subgroup.instFiniteSubtypeMem` `Sylow.isPGroup'` `eq_zero_or_pos` `Nat.instCanonicallyOrderedAdd` `card_mulAut` `pow_zero` `Nat.totient_one` `Nat.totient_prime_pow` `Fact.out` `Subgroup.relIndex_dvd_of_le_left` `Subgroup.le_centralizer` `instIsMulCommutativeSubtypeMemSubgroupOfIsCyclic` `Subgroup.relIndex_dvd_index_of_le` `Subgroup.le_normalizer` `Nat.Prime.coprime_iff_not_dvd` `Sylow.not_dvd_index` `SetLike.instFinite` `Subgroup.finiteIndex_of_finite` `Subgroup.relIndex_dvd_card` `Subgroup.card_subgroup_dvd_card` `tsub_pos_iff_lt` `Nat.instOrderedSub` `Nat.Prime.one_lt` `Mathlib.Tactic.Contrapose.contrapose₁` `Nat.minFac_pos` `Nat.minFac_le_of_dvd` `Nat.two_le_iff` `ne_zero_of_dvd_ne_zero` `LT.lt.ne'` `Nat.card_pos` `One.instNonempty` `dvd_rfl` `Subgroup.relIndex.eq_1` `Subgroup.index.eq_1` `Subgroup.normalizerMonoidHom_ker`

MonoidHom

Definitions

Name	Category	Theorems
`transfer` 📖	CompOp	4 math math: `transfer_def`, `transfer_center_eq_pow`, `transfer_eq_pow`, `transfer_eq_prod_quotient_orbitRel_zpowers_quot`
`transferCenterPow` 📖	CompOp	1 math math: `transferCenterPow_apply`
`transferSylow` 📖	CompOp	6 math math: `ker_transferSylow_disjoint`, `IsCyclic.isComplement'`, `transferSylow_eq_pow`, `ker_transferSylow_isComplement'`, `not_dvd_card_ker_transferSylow`, `transferSylow_restrict_eq_pow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ker_transferSylow_disjoint` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.normalizer` `Sylow.toSubgroup` `Subgroup.centralizer` `SetLike.coe` `Sylow` `Sylow.instSetLike` `IsPGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup`	`Disjoint` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Subgroup.instCompleteLattice` `ker` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `transferSylow`	—	`disjoint_iff` `Subgroup.card_eq_one` `IsPGroup.card_eq_or_dvd` `IsPGroup.to_le` `inf_le_right` `not_dvd_card_ker_transferSylow` `Dvd.dvd.trans` `Subgroup.card_dvd_of_le` `inf_le_left`
`ker_transferSylow_isComplement'` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.normalizer` `Sylow.toSubgroup` `Subgroup.centralizer` `SetLike.coe` `Sylow` `Sylow.instSetLike`	`Subgroup.IsComplement'` `ker` `SetLike.instMembership` `Subgroup.instSetLike` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `transferSylow`	—	`SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `Sylow.instSubgroupClass` `Equiv.bijective` `Sylow.isPGroup'` `Sylow.not_dvd_index` `transferSylow_restrict_eq_pow` `range_eq_top` `top_le_iff` `LE.le.trans` `Eq.ge` `restrict_range` `Function.Bijective.eq_1` `Subgroup.map_le_range` `Subgroup.isComplement'_of_disjoint_and_mul_eq_univ` `disjoint_iff` `Subgroup.coe_top` `Subgroup.map_bot` `Subgroup.subgroupOf_map_subtype` `ker_restrict` `Subgroup.map_injective` `Subgroup.subtype_injective` `ker_eq_bot_iff` `Subgroup.normal_mul` `normal_ker` `SetLike.ext'_iff` `sup_comm` `Subgroup.comap_map_eq` `Subgroup.comap_top` `Subgroup.comap_injective`
`not_dvd_card_ker_transferSylow` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.normalizer` `Sylow.toSubgroup` `Subgroup.centralizer` `SetLike.coe` `Sylow` `Sylow.instSetLike`	`Nat.card` `SetLike.instMembership` `Subgroup.instSetLike` `ker` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `transferSylow`	—	`Sylow.not_dvd_index` `Subgroup.IsComplement'.index_eq_card` `ker_transferSylow_isComplement'`
`transferCenterPow_apply` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.center` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `instFunLike` `transferCenterPow` `Monoid.toNatPow` `Subgroup.index`	—	—
`transferSylow_eq_pow` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.normalizer` `Sylow.toSubgroup` `Subgroup.centralizer` `SetLike.coe` `Sylow` `Sylow.instSetLike` `SetLike.instMembership`	`DFunLike.coe` `MonoidHom` `Subgroup.instSetLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `instFunLike` `transferSylow` `Monoid.toNatPow` `Subgroup.index` `transfer_eq_pow_aux` `transferSylow_eq_pow_aux`	—	`transfer_eq_pow` `transferSylow_eq_pow_aux`
`transferSylow_eq_pow_aux` 📖	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.normalizer` `Sylow.toSubgroup` `Subgroup.centralizer` `SetLike.coe` `Sylow` `Sylow.instSetLike` `SetLike.instMembership` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Monoid.toNatPow`	—	—	`Subgroup.pow_mem` `Sylow.conj_eq_normalizer_conj_of_mem` `Subgroup.le_normalizer` `Commute.inv_mul_cancel`
`transferSylow_restrict_eq_pow` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.normalizer` `Sylow.toSubgroup` `Subgroup.centralizer` `SetLike.coe` `Sylow` `Sylow.instSetLike`	`DFunLike.coe` `MonoidHom` `SetLike.instMembership` `Subgroup.instSetLike` `MulOneClass.toMulOne` `SubmonoidClass.toMulOneClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `Subgroup.toGroup` `instFunLike` `restrict` `transferSylow` `SubmonoidClass.nPow` `Sylow.instSubgroupClass` `Subgroup.index`	—	`SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `Sylow.instSubgroupClass` `transferSylow_eq_pow`
`transfer_center_eq_pow` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.center` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `CommGroup.ofIsMulCommutative` `Subgroup.toGroup` `Subgroup.center.isMulCommutative` `instFunLike` `transfer` `id` `Monoid.toNatPow` `Subgroup.index` `Subgroup.pow_index_mem` `Subgroup.instNormalCenter`	—	`transfer_eq_pow` `Subgroup.center.isMulCommutative` `LeftCancelSemigroup.toIsLeftCancelMul` `IsMulCentral.comm` `mul_inv_cancel_right`
`transfer_def` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instFunLike` `transfer` `Subgroup.leftTransversals.diff` `Subgroup.LeftTransversal` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Subgroup.instMulActionLeftTransversal` `Monoid.toMulAction` `MulAction.left_quotientAction`	—	`MulAction.left_quotientAction` `transfer.eq_1` `Subgroup.leftTransversals.diff_mul_diff` `Subgroup.leftTransversals.smul_diff_smul` `mul_comm`
`transfer_eq_pow` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Monoid.toNatPow`	`DFunLike.coe` `MonoidHom` `CommGroup.toGroup` `instFunLike` `transfer` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Subgroup.index` `transfer_eq_pow_aux`	—	`transfer_eq_pow_aux` `MulAction.left_quotientAction` `QuotientGroup.out_conj_pow_minimalPeriod_mem` `transfer_eq_prod_quotient_orbitRel_zpowers_quot` `Finset.prod_map_toList` `List.prod_map_hom` `instMonoidHomClass` `Subtype.coe_injective` `Subgroup.mem_zpowers` `Subgroup.coe_pow` `Subgroup.index_eq_card` `Nat.card_eq_fintype_card` `Fintype.card_congr` `Fintype.card_sigma` `Subgroup.zpowers_isMulCommutative` `Finset.prod_pow_eq_pow_sum` `Subgroup.val_list_prod`
`transfer_eq_pow_aux` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Monoid.toNatPow`	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.index`	—	`pow_zero` `Subgroup.one_mem` `MulAction.left_quotientAction` `QuotientGroup.out_conj_pow_minimalPeriod_mem` `Subgroup.mem_zpowers` `Subgroup.zpowers_isMulCommutative` `Subgroup.prod_mem` `Nat.card_eq_fintype_card` `Fintype.card_congr` `Fintype.card_sigma` `Finset.prod_congr` `MulAction.minimalPeriod_eq_card` `Finset.prod_pow_eq_pow_sum`
`transfer_eq_prod_quotient_orbitRel_zpowers_quot` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instFunLike` `transfer` `Finset.prod` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `MulAction.orbitRel` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `Subgroup.toGroup` `MulAction.mulLeftCosetsCompSubtypeVal` `CommGroup.toCommMonoid` `Finset.univ` `MulOne.toMul` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Quotient.out` `QuotientGroup.leftRel` `Monoid.toNatPow` `Function.minimalPeriod` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulAction.quotient` `Monoid.toMulAction` `MulAction.left_quotientAction` `QuotientGroup.out_conj_pow_minimalPeriod_mem`	—	`MulAction.left_quotientAction` `MulAction.minimalPeriod_pos` `Subtype.finite` `Subgroup.finite_quotient_of_finiteIndex` `QuotientGroup.out_conj_pow_minimalPeriod_mem` `transfer_def` `Equiv.prod_comp` `Finset.prod_sigma` `Fintype.prod_congr` `Subgroup.transferTransversal_apply'` `Subgroup.transferTransversal_apply''` `Finset.prod_congr` `Fintype.prod_eq_single` `inv_mul_cancel` `map_one` `MonoidHomClass.toOneHomClass` `instMonoidHomClass` `ZMod.cast_zero` `zpow_zero` `one_mul` `mul_assoc`

Subgroup

Definitions

Name	Category	Theorems
`transferFunction` 📖	CompOp	4 math math: `transferTransversal_apply`, `mem_transferSet`, `coe_transferFunction`, `transferFunction_apply`
`transferSet` 📖	CompOp	1 math math: `mem_transferSet`
`transferTransversal` 📖	CompOp	3 math math: `transferTransversal_apply`, `transferTransversal_apply'`, `transferTransversal_apply''`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_transferFunction` 📖	mathematical	—	`transferFunction`	—	`MulAction.left_quotientAction` `transferFunction_apply` `smul_eq_mul` `MulAction.Quotient.coe_smul_out` `quotientEquivSigmaZMod_symm_apply` `Sigma.eta` `Equiv.symm_apply_apply`
`mem_transferSet` 📖	mathematical	—	`Set` `Set.instMembership` `transferSet` `transferFunction`	—	—
`transferFunction_apply` 📖	mathematical	—	`transferFunction` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DivInvMonoid.toZPow` `ZMod.cast` `Ring.toAddGroupWithOne` `Int.instRing` `Function.minimalPeriod` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulAction.quotient` `Monoid.toMulAction` `MulAction.left_quotientAction` `Quotient.out` `MulAction.orbitRel` `SetLike.instMembership` `instSetLike` `zpowers` `toGroup` `MulAction.mulLeftCosetsCompSubtypeVal` `MulAction.orbitRel.Quotient` `ZMod` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `quotientEquivSigmaZMod` `QuotientGroup.leftRel`	—	—
`transferTransversal_apply` 📖	mathematical	—	`Set` `Set.instMembership` `IsComplement` `SetLike.coe` `Subgroup` `instSetLike` `transferTransversal` `DFunLike.coe` `Equiv` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `IsComplement.leftQuotientEquiv` `transferFunction`	—	`IsComplement.leftQuotientEquiv_apply` `coe_transferFunction`
`transferTransversal_apply'` 📖	mathematical	—	`Set` `Set.instMembership` `IsComplement` `SetLike.coe` `Subgroup` `instSetLike` `transferTransversal` `DFunLike.coe` `Equiv` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `IsComplement.leftQuotientEquiv` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MulAction.quotient` `Monoid.toMulAction` `MulAction.left_quotientAction` `DivInvMonoid.toZPow` `ZMod.cast` `Ring.toAddGroupWithOne` `Int.instRing` `Function.minimalPeriod` `Quotient.out` `MulAction.orbitRel` `SetLike.instMembership` `zpowers` `toGroup` `MulAction.mulLeftCosetsCompSubtypeVal` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `QuotientGroup.leftRel`	—	`MulAction.left_quotientAction` `transferTransversal_apply` `transferFunction_apply` `quotientEquivSigmaZMod_symm_apply` `Equiv.apply_symm_apply`
`transferTransversal_apply''` 📖	mathematical	—	`Set` `Set.instMembership` `IsComplement` `SetLike.coe` `Subgroup` `instSetLike` `LeftTransversal` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `instMulActionLeftTransversal` `Monoid.toMulAction` `MulAction.left_quotientAction` `transferTransversal` `DFunLike.coe` `Equiv` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `IsComplement.leftQuotientEquiv` `MulAction.quotient` `DivInvMonoid.toZPow` `ZMod.cast` `Ring.toAddGroupWithOne` `Int.instRing` `Function.minimalPeriod` `Quotient.out` `MulAction.orbitRel` `SetLike.instMembership` `zpowers` `toGroup` `MulAction.mulLeftCosetsCompSubtypeVal` `ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `ZMod.decidableEq` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toNatPow` `QuotientGroup.leftRel`	—	`MulAction.left_quotientAction` `smul_apply_eq_smul_apply_inv_smul` `transferTransversal_apply` `transferFunction_apply` `SemigroupAction.mul_smul` `zpow_neg_one` `zpow_add` `quotientEquivSigmaZMod_apply` `smul_eq_mul` `mul_assoc` `zpow_one_add` `Int.cast_add` `Int.cast_neg` `Int.cast_one` `ZMod.intCast_cast` `ZMod.cast_id'` `sub_eq_neg_add` `ZMod.cast_sub_one` `add_sub_cancel` `zpow_natCast`

Subgroup.leftTransversals

Definitions

Name	Category	Theorems
`diff` 📖	CompOp	7 math math: `diff_self`, `Subgroup.smul_diff_smul'`, `MonoidHom.transfer_def`, `diff_mul_diff`, `smul_diff_smul`, `diff_inv`, `Subgroup.smul_diff'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diff_inv` 📖	mathematical	—	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `diff`	—	`inv_eq_of_mul_eq_one_right` `diff_mul_diff` `diff_self`
`diff_mul_diff` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `diff`	—	`Finset.prod_mul_distrib` `Finset.prod_congr` `MonoidHom.map_mul` `mul_assoc` `mul_inv_cancel_left`
`diff_self` 📖	mathematical	—	`diff` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	`mul_eq_left` `LeftCancelSemigroup.toIsLeftCancelMul` `diff_mul_diff`
`smul_diff_smul` 📖	mathematical	—	`diff` `Subgroup.LeftTransversal` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Subgroup.instMulActionLeftTransversal` `Monoid.toMulAction` `MulAction.left_quotientAction`	—	`Fintype.prod_equiv` `MulAction.left_quotientAction` `Subgroup.smul_apply_eq_smul_apply_inv_smul` `mul_inv_rev` `mul_assoc` `inv_mul_cancel_left`

---

← Back to Index