Documentation Verification Report

Schreier

📁 Source: Mathlib/GroupTheory/Schreier.lean

Statistics

Metric	Count
Definitions `cardCommutatorBound`	1
Theorems `card_commutator_dvd_index_center_pow`, `card_commutator_le_of_finite_commutatorSet`, `closure_mul_image_eq`, `closure_mul_image_eq_top`, `closure_mul_image_eq_top'`, `closure_mul_image_mul_eq_top`, `exists_finset_card_le_mul`, `fg_of_index_ne_zero`, `instFiniteSubtypeMemCommutatorOfElemCommutatorSet`, `rank_le_index_mul_rank`, `card_dvd_exponent_nsmul_rank`, `card_dvd_exponent_nsmul_rank'`, `card_dvd_exponent_pow_rank`, `card_dvd_exponent_pow_rank'`	14
Total	15

Subgroup

Definitions

Name	Category	Theorems
`cardCommutatorBound` 📖	CompOp	1 math math: `card_commutator_le_of_finite_commutatorSet`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_commutator_dvd_index_center_pow` 📖	mathematical	—	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike` `commutator` `Monoid.toPow` `Nat.instMonoid` `index` `center` `Set.Elem` `commutatorSet`	—	`MulZeroClass.zero_mul` `zero_add` `pow_one` `card_mul_index` `pow_succ` `relIndex_dvd_index_of_normal` `instNormalCenter` `mul_dvd_mul` `fg_of_index_ne_zero` `instFGSubtypeMemCommutator` `ne_zero_of_dvd_ne_zero` `rank_le_index_mul_rank` `rank_commutator_le_card` `dvd_trans` `card_dvd_exponent_pow_rank'` `subgroupOf_isMulCommutative` `center.isMulCommutative` `Abelianization.commutator_subset_ker` `pow_dvd_pow` `LE.le.trans`
`card_commutator_le_of_finite_commutatorSet` 📖	mathematical	—	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike` `commutator` `cardCommutatorBound` `Set.Elem` `commutatorSet`	—	`closureCommutatorRepresentatives_fg` `index_center_le_pow` `instFiniteElemSubtypeMemSubgroupClosureCommutatorRepresentativesCommutatorSet` `card_commutator_dvd_index_center_pow` `LE.le.trans` `card_commutatorSet_closureCommutatorRepresentatives` `Finite.card_pos` `instNonemptyElemCommutatorSet` `rank_closureCommutatorRepresentatives_le` `Dvd.dvd.trans` `card_commutator_closureCommutatorRepresentatives` `pow_dvd_pow` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `Nat.instMulLeftMono` `pow_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.instZeroLEOneClass` `FiniteIndex.index_ne_zero` `finiteIndex_center` `pow_succ`
`closure_mul_image_eq` 📖	mathematical	`IsComplement` `SetLike.coe` `Subgroup` `instSetLike` `Set` `Set.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `closure` `Top.top` `instTop`	`closure` `Set.image` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Set` `Set.instMembership` `IsComplement.toRightFun` `Set.mul`	—	`closure_le` `IsComplement.mul_inv_toRightFun_mem` `le_antisymm` `eq_top_iff` `closure_mul_image_mul_eq_top` `mem_top` `ExistsUnique.unique` `isComplement_iff_existsUnique_mul_inv_mem` `mul_inv_cancel` `one_mem` `inv_one` `mul_one` `mul_mem_cancel_left`
`closure_mul_image_eq_top` 📖	mathematical	`IsComplement` `SetLike.coe` `Subgroup` `instSetLike` `Set` `Set.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `closure` `Top.top` `instTop`	`closure` `Subgroup` `SetLike.instMembership` `instSetLike` `toGroup` `Set.image` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Set` `Set.instMembership` `IsComplement.toRightFun` `IsComplement.mul_inv_toRightFun_mem` `Set.mul` `Top.top` `instTop`	—	`IsComplement.mul_inv_toRightFun_mem` `eq_top_iff` `map_subtype_le_map_subtype` `MonoidHom.map_closure` `Set.image_image` `LE.le.trans` `map_subtype_le` `ge_of_eq` `closure_mul_image_eq`
`closure_mul_image_eq_top'` 📖	mathematical	`IsComplement` `SetLike.coe` `Subgroup` `instSetLike` `Finset` `Finset.instSetLike` `SetLike.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `closure` `Top.top` `instTop`	`closure` `Subgroup` `SetLike.instMembership` `instSetLike` `toGroup` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.image` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Set` `Set.instMembership` `IsComplement.toRightFun` `IsComplement.mul_inv_toRightFun_mem` `Finset.mul` `Top.top` `instTop`	—	`IsComplement.mul_inv_toRightFun_mem` `Finset.coe_image` `Finset.coe_mul` `closure_mul_image_eq_top`
`closure_mul_image_mul_eq_top` 📖	mathematical	`IsComplement` `SetLike.coe` `Subgroup` `instSetLike` `Set` `Set.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `closure` `Top.top` `instTop`	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `Subgroup` `instSetLike` `closure` `Set.image` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Set.instMembership` `IsComplement.toRightFun` `Top.top` `BooleanAlgebra.toTop` `Set.instBooleanAlgebra`	—	`top_le_iff` `closure_induction_right` `one_mem` `one_mul` `Mathlib.Tactic.Group.zpow_trick_one'` `neg_add_cancel` `zpow_zero` `mul_one` `Set.mul_mem_mul` `mul_mem` `subset_closure` `Subtype.coe_prop` `mul_zpow_neg_one` `neg_neg` `zpow_one` `inv_mem` `LeftCancelSemigroup.toIsLeftCancelMul` `ExistsUnique.unique` `isComplement_iff_existsUnique_mul_inv_mem` `IsComplement.mul_inv_toRightFun_mem` `mul_assoc` `inv_inv` `mul_inv_rev` `IsComplement.toRightFun_mul_inv_mem` `eq_top_iff` `mem_top`
`exists_finset_card_le_mul` 📖	mathematical	`closure` `SetLike.coe` `Finset` `Finset.instSetLike` `Top.top` `Subgroup` `instTop`	`Finset` `Subgroup` `SetLike.instMembership` `instSetLike` `Finset.card` `index` `closure` `toGroup` `SetLike.coe` `Finset.instSetLike` `Top.top` `instTop`	—	`exists_isComplement_right` `Set.coe_toFinset` `Set.mem_toFinset` `IsComplement.mul_inv_toRightFun_mem` `Finset.card_image_le` `Finset.card_mul_le` `Fintype.card_coe` `Fintype.card_congr` `QuotientGroup.card_quotient_rightRel` `index_eq_card` `Nat.card_eq_fintype_card` `closure_mul_image_eq_top'`
`fg_of_index_ne_zero` 📖	mathematical	—	`Group.FG` `Subgroup` `SetLike.instMembership` `instSetLike` `toGroup`	—	`Group.FG.out` `exists_finset_card_le_mul`
`instFiniteSubtypeMemCommutatorOfElemCommutatorSet` 📖	mathematical	—	`Finite` `Subgroup` `SetLike.instMembership` `instSetLike` `commutator`	—	`card_commutator_dvd_index_center_pow` `instFiniteElemSubtypeMemSubgroupClosureCommutatorRepresentativesCommutatorSet` `Nat.finite_of_card_ne_zero` `FiniteIndex.index_ne_zero` `finiteIndex_center` `closureCommutatorRepresentatives_fg` `eq_zero_of_pow_eq_zero` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `Nat.instIsDomain` `zero_dvd_iff` `card_commutator_closureCommutatorRepresentatives`
`rank_le_index_mul_rank` 📖	mathematical	—	`Group.rank` `Subgroup` `SetLike.instMembership` `instSetLike` `toGroup` `fg_of_index_ne_zero` `index`	—	`fg_of_index_ne_zero` `Group.rank_spec` `exists_finset_card_le_mul` `Group.rank_le`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_dvd_exponent_nsmul_rank` 📖	mathematical	—	`Nat.card` `Monoid.toPow` `Nat.instMonoid` `AddMonoid.exponent` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddGroup.rank`	—	`AddGroup.rank_spec` `Fintype.card_coe` `Finset.card_univ` `Finset.prod_const` `add_comm` `AddMonoidHom.range_eq_top` `eq_top_iff` `AddSubgroup.closure_le` `AddSubgroup.mem_zmultiples` `AddSubgroup.noncommPiCoprod_single` `AddSubgroup.card_dvd_of_surjective` `Dvd.dvd.trans` `Nat.card_pi` `Finset.prod_dvd_prod_of_dvd` `Nat.card_zmultiples` `AddMonoid.addOrder_dvd_exponent`
`card_dvd_exponent_nsmul_rank'` 📖	mathematical	`AddMonoid.toNSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Nat.card` `Monoid.toPow` `Nat.instMonoid` `AddGroup.rank` `AddCommGroup.toAddGroup`	—	`Dvd.dvd.trans` `card_dvd_exponent_nsmul_rank` `pow_dvd_pow_of_dvd` `AddMonoid.exponent_dvd_of_forall_nsmul_eq_zero`
`card_dvd_exponent_pow_rank` 📖	mathematical	—	`Nat.card` `Monoid.toPow` `Nat.instMonoid` `Monoid.exponent` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Group.rank`	—	`Group.rank_spec` `Fintype.card_coe` `Finset.card_univ` `Finset.prod_const` `mul_comm` `MonoidHom.range_eq_top` `eq_top_iff` `Subgroup.closure_le` `Subgroup.mem_zpowers` `Subgroup.noncommPiCoprod_mulSingle` `Subgroup.card_dvd_of_surjective` `Dvd.dvd.trans` `Nat.card_pi` `Finset.prod_dvd_prod_of_dvd` `Nat.card_zpowers` `Monoid.order_dvd_exponent`
`card_dvd_exponent_pow_rank'` 📖	mathematical	`Monoid.toPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	`Nat.card` `Monoid.toPow` `Nat.instMonoid` `Group.rank` `CommGroup.toGroup`	—	`Dvd.dvd.trans` `card_dvd_exponent_pow_rank` `pow_dvd_pow_of_dvd` `Monoid.exponent_dvd_of_forall_pow_eq_one`

---

← Back to Index