Documentation Verification Report

SchurZassenhaus

📁 Source: Mathlib/GroupTheory/SchurZassenhaus.lean

Statistics

Metric	Count
Definitions `QuotientDiff`, `instInhabitedQuotientDiff`, `instMulActionQuotientDiff`	3
Theorems `step7`, `eq_one_of_smul_eq_one`, `exists_left_complement'_of_coprime`, `exists_right_complement'_of_coprime`, `exists_smul_eq`, `isComplement'_stabilizer_of_coprime`, `smul_diff'`, `smul_diff_smul'`	8
Total	11

Subgroup

Definitions

Name	Category	Theorems
`QuotientDiff` 📖	CompOp	2 math math: `exists_smul_eq`, `isComplement'_stabilizer_of_coprime`
`instInhabitedQuotientDiff` 📖	CompOp	—
`instMulActionQuotientDiff` 📖	CompOp	2 math math: `exists_smul_eq`, `isComplement'_stabilizer_of_coprime`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_one_of_smul_eq_one` 📖	mathematical	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike` `index` `QuotientDiff` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `MulAction.toSemigroupAction` `instMulAction` `instMulActionQuotientDiff`	`one`	—	`Quotient.inductionOn'` `Equiv.injective` `MulAction.right_quotientAction'` `leftTransversals.diff_inv` `smul_diff'` `leftTransversals.diff_self` `one_mul` `inv_pow` `inv_inv` `Quotient.exact'` `one_pow`
`exists_left_complement'_of_coprime` 📖	mathematical	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike` `index`	`IsComplement'`	—	`IsComplement'.symm` `exists_right_complement'_of_coprime`
`exists_right_complement'_of_coprime` 📖	mathematical	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike` `index`	`IsComplement'`	—	`index_eq_one` `isComplement'_top_bot` `Nat.card_eq_one_iff_unique` `eq_bot_of_subsingleton` `isComplement'_bot_top` `Nat.finite_of_card_ne_zero` `card_mul_index` `mul_ne_zero` `IsDomain.to_noZeroDivisors` `Nat.instIsDomain`
`exists_smul_eq` 📖	mathematical	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike` `index`	`QuotientDiff` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `MulAction.toSemigroupAction` `instMulAction` `instMulActionQuotientDiff`	—	`Quotient.inductionOn'` `MulAction.right_quotientAction'` `Quotient.sound'` `leftTransversals.diff_inv` `inv_eq_one` `smul_diff'` `inv_pow` `powCoprime_apply` `Equiv.apply_symm_apply` `mul_inv_cancel`
`isComplement'_stabilizer_of_coprime` 📖	mathematical	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike` `index`	`IsComplement'` `MulAction.stabilizer` `QuotientDiff` `instMulActionQuotientDiff`	—	`isComplement'_stabilizer` `eq_one_of_smul_eq_one` `exists_smul_eq`
`smul_diff'` 📖	mathematical	—	`leftTransversals.diff` `Subgroup` `SetLike.instMembership` `instSetLike` `CommGroup.ofIsMulCommutative` `toGroup` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulOpposite` `LeftTransversal` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulOpposite.instMonoid` `MulAction.toSemigroupAction` `instMulActionLeftTransversal` `MulOpposite.instGroup` `Monoid.toOppositeMulAction` `MulAction.right_quotientAction'` `MulOpposite.op` `mul` `npow` `index`	—	`MulAction.right_quotientAction'` `leftTransversals.diff.eq_1` `index_eq_card` `Nat.card_eq_fintype_card` `Finset.card_univ` `Finset.prod_const` `Finset.prod_mul_distrib` `Finset.prod_congr` `mul_assoc` `LeftCancelSemigroup.toIsLeftCancelMul` `smul_apply_eq_smul_apply_inv_smul` `MulOpposite.smul_eq_mul_unop` `MulOpposite.unop_op` `RightCancelSemigroup.toIsRightCancelMul` `Equiv.apply_eq_iff_eq` `inv_smul_eq_iff` `left_eq_mul` `QuotientGroup.eq_one_iff`
`smul_diff_smul'` 📖	mathematical	—	`leftTransversals.diff` `Subgroup` `SetLike.instMembership` `instSetLike` `CommGroup.ofIsMulCommutative` `toGroup` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulOpposite` `LeftTransversal` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulOpposite.instMonoid` `MulAction.toSemigroupAction` `instMulActionLeftTransversal` `MulOpposite.instGroup` `Monoid.toOppositeMulAction` `MulAction.right_quotientAction'` `MulOne.toMul` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MulOpposite.unop` `Normal.mem_comm` `DivInvMonoid.toInv` `mul_inv_cancel_left` `SetLike.coe_mem`	—	`Normal.mem_comm` `mul_inv_cancel_left` `SetLike.coe_mem` `coe_one` `mul_one` `inv_mul_cancel` `mul_assoc` `MulAction.right_quotientAction'` `Fintype.prod_equiv` `smul_apply_eq_smul_apply_inv_smul` `mul_inv_rev` `map_prod` `MonoidHom.instMonoidHomClass`

Subgroup.SchurZassenhausInduction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`step7` 📖	mathematical	`Nat.card` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.index` `Subgroup.IsComplement'`	`IsMulCommutative` `Subgroup.mul`	—	`Commute.symm` `IsMulCentral.comm` `eq_top_iff` `ConjAct.normal_of_characteristic_of_normal` `Subgroup.centerCharacteristic` `LT.lt.ne'` `IsPGroup.bot_lt_center` `Subgroup.bot_or_nontrivial` `Subgroup.instFiniteSubtypeMem` `Subgroup.mem_top`

---

← Back to Index