Documentation Verification Report

NoncommPiCoprod

📁 Source: Mathlib/GroupTheory/NoncommPiCoprod.lean

Statistics

Metric	Count
Definitions `noncommPiCoprod`, `noncommPiCoprodEquiv`, `noncommPiCoprod`, `noncommPiCoprod`, `noncommPiCoprodEquiv`, `noncommPiCoprod`	6
Theorems `addCommute_noncommPiCoprod`, `comp_noncommPiCoprod`, `independent_range_of_coprime_order`, `injective_noncommPiCoprod_of_iSupIndep`, `noncommPiCoprod_apply`, `noncommPiCoprod_mrange`, `noncommPiCoprod_range`, `noncommPiCoprod_single`, `addCommute_subtype_of_addCommute`, `eq_zero_of_noncommSum_eq_zero_of_iSupIndep`, `independent_of_coprime_order`, `injective_noncommPiCoprod_of_iSupIndep`, `noncommPiCoprod_apply`, `noncommPiCoprod_range`, `noncommPiCoprod_single`, `commute_noncommPiCoprod`, `comp_noncommPiCoprod`, `independent_range_of_coprime_order`, `injective_noncommPiCoprod_of_iSupIndep`, `noncommPiCoprod_apply`, `noncommPiCoprod_mrange`, `noncommPiCoprod_mulSingle`, `noncommPiCoprod_range`, `commute_subtype_of_commute`, `eq_one_of_noncommProd_eq_one_of_iSupIndep`, `independent_of_coprime_order`, `injective_noncommPiCoprod_of_iSupIndep`, `noncommPiCoprod_apply`, `noncommPiCoprod_mulSingle`, `noncommPiCoprod_range`	30
Total	36

AddMonoidHom

Definitions

Name	Category	Theorems
`noncommPiCoprod` 📖	CompOp	7 math math: `noncommPiCoprod_apply`, `noncommPiCoprod_range`, `comp_noncommPiCoprod`, `addCommute_noncommPiCoprod`, `noncommPiCoprod_mrange`, `noncommPiCoprod_single`, `injective_noncommPiCoprod_of_iSupIndep`
`noncommPiCoprodEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addCommute_noncommPiCoprod` 📖	mathematical	`Pairwise` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `AddMonoidHom` `instFunLike`	`Pi.addZeroClass` `noncommPiCoprod`	—	`Finset.noncommSum_induction` `AddCommute.add_right` `AddCommute.zero_right`
`comp_noncommPiCoprod` 📖	mathematical	`Pairwise` `Pairwise.mono`	`comp` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `noncommPiCoprod`	—	`ext` `AddCommute.map` `AddMonoidHomClass.toAddHomClass` `instAddMonoidHomClass` `Set.Pairwise.of_refl` `AddCommute.on_refl` `Finset.map_noncommSum` `Finset.noncommSum_congr`
`independent_range_of_coprime_order` 📖	mathematical	`Pairwise` `Fintype.card`	`iSupIndep` `AddSubgroup` `AddSubgroup.instCompleteLattice` `range`	—	`nonempty_fintype` `disjoint_iff_inf_le` `noncommPiCoprod_range` `iSup_subtype'` `Dvd.dvd.trans` `addOrderOf_map_dvd` `addOrderOf_dvd_card` `Fintype.card_pi` `one_nsmul` `addOrderOf_dvd_iff_nsmul_eq_zero` `Nat.coprime_fintype_prod_left_iff`
`injective_noncommPiCoprod_of_iSupIndep` 📖	mathematical	`Pairwise` `iSupIndep` `AddSubgroup` `AddSubgroup.instCompleteLattice` `range` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLike`	`Pi.addZeroClass` `noncommPiCoprod`	—	`ker_eq_bot_iff` `eq_bot_iff` `AddSubgroup.eq_zero_of_noncommSum_eq_zero_of_iSupIndep` `Finset.mem_univ` `mem_range` `map_zero` `AddMonoidHomClass.toZeroHomClass` `instAddMonoidHomClass`
`noncommPiCoprod_apply` 📖	mathematical	`Pairwise`	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `instFunLike` `noncommPiCoprod` `Finset.noncommSum` `Finset.univ` `Pairwise.set_pairwise` `AddCommute` `AddZero.toAdd` `SetLike.coe` `Finset` `Finset.instSetLike`	—	—
`noncommPiCoprod_mrange` 📖	mathematical	`Pairwise`	`mrange` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidHom` `AddZeroClass.toAddZero` `instFunLike` `instAddMonoidHomClass` `noncommPiCoprod` `iSup` `AddSubmonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `AddSubmonoid.instCompleteLattice`	—	`le_antisymm` `instAddMonoidHomClass` `AddSubmonoid.noncommSum_mem` `AddSubmonoid.mem_sSup_of_mem` `mem_mrange` `iSup_le` `noncommPiCoprod_single`
`noncommPiCoprod_range` 📖	mathematical	`Pairwise`	`range` `Pi.addGroup` `noncommPiCoprod` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `iSup` `AddSubgroup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `AddSubgroup.instCompleteLattice`	—	`le_antisymm` `AddSubgroup.noncommSum_mem` `AddSubgroup.mem_sSup_of_mem` `mem_range` `iSup_le` `noncommPiCoprod_single`
`noncommPiCoprod_single` 📖	mathematical	`Pairwise`	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `instFunLike` `noncommPiCoprod` `Pi.single` `AddZero.toZero`	—	`Finset.insert_erase` `Finset.mem_univ` `Set.Pairwise.mono` `Finset.mem_insert_of_mem` `Finset.noncommSum_insert_of_notMem` `Finset.notMem_erase` `Pi.single_eq_same` `Finset.noncommSum_eq_card_nsmul` `Pi.single_eq_of_ne` `Finset.mem_erase` `map_zero` `AddMonoidHomClass.toZeroHomClass` `instAddMonoidHomClass` `nsmul_zero` `add_zero`

AddSubgroup

Definitions

Name	Category	Theorems
`noncommPiCoprod` 📖	CompOp	4 math math: `noncommPiCoprod_single`, `noncommPiCoprod_range`, `noncommPiCoprod_apply`, `injective_noncommPiCoprod_of_iSupIndep`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addCommute_subtype_of_addCommute` 📖	mathematical	`Pairwise`	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DFunLike.coe` `AddMonoidHom` `AddSubgroup` `SetLike.instMembership` `instSetLike` `toAddGroup` `AddMonoidHom.instFunLike` `subtype`	—	—
`eq_zero_of_noncommSum_eq_zero_of_iSupIndep` 📖	—	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.onFun` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `iSupIndep` `AddSubgroup` `instCompleteLattice` `SetLike.instMembership` `instSetLike` `Finset.noncommSum` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Finset.instMembership`	—	—	`Finset.induction_on` `Finset.notMem_empty` `IsEmpty.forall_iff` `instIsEmptyFalse` `Set.Pairwise.mono` `Finset.coe_subset` `Finset.subset_insert` `noncommSum_mem` `le_iSup₂` `Finset.forall_mem_insert` `SetLike.mem_coe` `disjoint_iff_add_eq_zero` `iSupIndep.disjoint_biSup` `Finset.mem_insert_of_mem` `Finset.noncommSum_insert_of_notMem` `Finset.mem_insert`
`independent_of_coprime_order` 📖	mathematical	`Pairwise` `Fintype.card` `AddSubgroup` `SetLike.instMembership` `instSetLike`	`iSupIndep` `instCompleteLattice`	—	`range_subtype` `AddMonoidHom.independent_range_of_coprime_order` `addCommute_subtype_of_addCommute`
`injective_noncommPiCoprod_of_iSupIndep` 📖	mathematical	`Pairwise` `iSupIndep` `AddSubgroup` `instCompleteLattice`	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `SetLike.instMembership` `instSetLike` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddGroup` `AddMonoidHom.instFunLike` `noncommPiCoprod`	—	`AddMonoidHom.injective_noncommPiCoprod_of_iSupIndep` `addCommute_subtype_of_addCommute` `range_subtype` `Subtype.coe_injective`
`noncommPiCoprod_apply` 📖	mathematical	`Pairwise`	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddSubgroup` `SetLike.instMembership` `instSetLike` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddGroup` `AddMonoidHom.instFunLike` `noncommPiCoprod` `Finset.noncommSum` `Finset.univ` `Subtype.prop`	—	`Subtype.prop` `addCommute_subtype_of_addCommute` `Finset.noncommSum_congr`
`noncommPiCoprod_range` 📖	mathematical	`Pairwise`	`AddMonoidHom.range` `Pi.addGroup` `AddSubgroup` `SetLike.instMembership` `instSetLike` `toAddGroup` `noncommPiCoprod` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`addCommute_subtype_of_addCommute` `AddMonoidHom.noncommPiCoprod_range` `range_subtype`
`noncommPiCoprod_single` 📖	mathematical	`Pairwise`	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddSubgroup` `SetLike.instMembership` `instSetLike` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddGroup` `AddMonoidHom.instFunLike` `noncommPiCoprod` `Pi.single` `zero`	—	`AddMonoidHom.noncommPiCoprod_single` `addCommute_subtype_of_addCommute`

MonoidHom

Definitions

Name	Category	Theorems
`noncommPiCoprod` 📖	CompOp	7 math math: `noncommPiCoprod_apply`, `noncommPiCoprod_mulSingle`, `noncommPiCoprod_mrange`, `comp_noncommPiCoprod`, `noncommPiCoprod_range`, `injective_noncommPiCoprod_of_iSupIndep`, `commute_noncommPiCoprod`
`noncommPiCoprodEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commute_noncommPiCoprod` 📖	mathematical	`Pairwise` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DFunLike.coe` `MonoidHom` `instFunLike`	`Pi.mulOneClass` `noncommPiCoprod`	—	`Finset.noncommProd_induction` `Commute.mul_right` `Commute.one_right`
`comp_noncommPiCoprod` 📖	mathematical	`Pairwise` `Pairwise.mono`	`comp` `MulOneClass.toMulOne` `Pi.mulOneClass` `Monoid.toMulOneClass` `noncommPiCoprod`	—	`ext` `Commute.map` `MonoidHomClass.toMulHomClass` `instMonoidHomClass` `Set.Pairwise.of_refl` `Commute.on_refl` `Finset.map_noncommProd` `Finset.noncommProd_congr`
`independent_range_of_coprime_order` 📖	mathematical	`Pairwise` `Fintype.card`	`iSupIndep` `Subgroup` `Subgroup.instCompleteLattice` `range`	—	`nonempty_fintype` `disjoint_iff_inf_le` `noncommPiCoprod_range` `iSup_subtype'` `Dvd.dvd.trans` `orderOf_map_dvd` `orderOf_dvd_card` `Fintype.card_pi` `pow_one` `orderOf_dvd_iff_pow_eq_one` `Nat.coprime_fintype_prod_left_iff`
`injective_noncommPiCoprod_of_iSupIndep` 📖	mathematical	`Pairwise` `iSupIndep` `Subgroup` `Subgroup.instCompleteLattice` `range` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instFunLike`	`Pi.mulOneClass` `noncommPiCoprod`	—	`ker_eq_bot_iff` `eq_bot_iff` `Subgroup.eq_one_of_noncommProd_eq_one_of_iSupIndep` `Finset.mem_univ` `map_one` `MonoidHomClass.toOneHomClass` `instMonoidHomClass`
`noncommPiCoprod_apply` 📖	mathematical	`Pairwise`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Pi.mulOneClass` `Monoid.toMulOneClass` `instFunLike` `noncommPiCoprod` `Finset.noncommProd` `Finset.univ` `Pairwise.set_pairwise` `Commute` `MulOne.toMul` `SetLike.coe` `Finset` `Finset.instSetLike`	—	—
`noncommPiCoprod_mrange` 📖	mathematical	`Pairwise`	`mrange` `Pi.mulOneClass` `Monoid.toMulOneClass` `MonoidHom` `MulOneClass.toMulOne` `instFunLike` `instMonoidHomClass` `noncommPiCoprod` `iSup` `Submonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submonoid.instCompleteLattice`	—	`le_antisymm` `instMonoidHomClass` `Submonoid.noncommProd_mem` `Submonoid.mem_sSup_of_mem` `iSup_le` `noncommPiCoprod_mulSingle`
`noncommPiCoprod_mulSingle` 📖	mathematical	`Pairwise`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Pi.mulOneClass` `Monoid.toMulOneClass` `instFunLike` `noncommPiCoprod` `Pi.mulSingle` `MulOne.toOne`	—	`Finset.insert_erase` `Finset.mem_univ` `Set.Pairwise.mono` `Finset.mem_insert_of_mem` `Finset.noncommProd_insert_of_notMem` `Finset.notMem_erase` `Pi.mulSingle_eq_same` `Finset.noncommProd_eq_pow_card` `Pi.mulSingle_eq_of_ne` `map_one` `MonoidHomClass.toOneHomClass` `instMonoidHomClass` `one_pow` `mul_one`
`noncommPiCoprod_range` 📖	mathematical	`Pairwise`	`range` `Pi.group` `noncommPiCoprod` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `iSup` `Subgroup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Subgroup.instCompleteLattice`	—	`le_antisymm` `Subgroup.noncommProd_mem` `Subgroup.mem_sSup_of_mem` `iSup_le` `noncommPiCoprod_mulSingle`

Subgroup

Definitions

Name	Category	Theorems
`noncommPiCoprod` 📖	CompOp	6 math math: `Equiv.Perm.disjoint_ofSubtype_noncommPiCoprod`, `noncommPiCoprod_apply`, `injective_noncommPiCoprod_of_iSupIndep`, `noncommPiCoprod_mulSingle`, `noncommPiCoprod_range`, `Equiv.Perm.commute_ofSubtype_noncommPiCoprod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commute_subtype_of_commute` 📖	mathematical	`Pairwise`	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DFunLike.coe` `MonoidHom` `Subgroup` `SetLike.instMembership` `instSetLike` `toGroup` `MonoidHom.instFunLike` `subtype`	—	—
`eq_one_of_noncommProd_eq_one_of_iSupIndep` 📖	—	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `iSupIndep` `Subgroup` `instCompleteLattice` `SetLike.instMembership` `instSetLike` `Finset.noncommProd` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Finset.instMembership`	—	—	`Finset.induction_on` `instIsEmptyFalse` `Set.Pairwise.mono` `Finset.coe_subset` `Finset.subset_insert` `noncommProd_mem` `le_iSup₂` `disjoint_iff_mul_eq_one` `iSupIndep.disjoint_biSup` `Finset.mem_insert_of_mem` `Finset.noncommProd_insert_of_notMem`
`independent_of_coprime_order` 📖	mathematical	`Pairwise` `Fintype.card` `Subgroup` `SetLike.instMembership` `instSetLike`	`iSupIndep` `instCompleteLattice`	—	`range_subtype` `MonoidHom.independent_range_of_coprime_order` `commute_subtype_of_commute`
`injective_noncommPiCoprod_of_iSupIndep` 📖	mathematical	`Pairwise` `iSupIndep` `Subgroup` `instCompleteLattice`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Pi.mulOneClass` `SetLike.instMembership` `instSetLike` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `MonoidHom.instFunLike` `noncommPiCoprod`	—	`MonoidHom.injective_noncommPiCoprod_of_iSupIndep` `commute_subtype_of_commute` `range_subtype` `Subtype.coe_injective`
`noncommPiCoprod_apply` 📖	mathematical	`Pairwise`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Pi.mulOneClass` `Subgroup` `SetLike.instMembership` `instSetLike` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `MonoidHom.instFunLike` `noncommPiCoprod` `Finset.noncommProd` `Finset.univ` `Subtype.prop`	—	`Subtype.prop` `commute_subtype_of_commute` `Finset.noncommProd_congr`
`noncommPiCoprod_mulSingle` 📖	mathematical	`Pairwise`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Pi.mulOneClass` `Subgroup` `SetLike.instMembership` `instSetLike` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `MonoidHom.instFunLike` `noncommPiCoprod` `Pi.mulSingle` `one`	—	`MonoidHom.noncommPiCoprod_mulSingle` `commute_subtype_of_commute`
`noncommPiCoprod_range` 📖	mathematical	`Pairwise`	`MonoidHom.range` `Pi.group` `Subgroup` `SetLike.instMembership` `instSetLike` `toGroup` `noncommPiCoprod` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`commute_subtype_of_commute` `MonoidHom.noncommPiCoprod_range` `range_subtype`

---

← Back to Index