Documentation Verification Report

Focal

📁 Source: Mathlib/GroupTheory/Focal.lean

Statistics

Metric	Count
Definitions `focalAddSubgroup`, `focalAddSubgroupOf`, `transferFocal`, `focalSubgroup`, `focalSubgroupOf`, `transferFocal`, `quotientKerMulEquivQuotientFocalSubroupOf`	7
Theorems `addCommutator_le_focalAddSubgroup`, `addCommutator_le_focalAddSubgroupOf`, `mk'_addConj_eq`, `focalAddSubgroupOf_def`, `focalAddSubgroupOf_eq_closure`, `focalAddSubgroup_def`, `focalAddSubgroup_le`, `focalAddSubgroup_le_addCommutator`, `instIsAddCommutativeQuotientSubtypeMemFocalAddSubgroupOf`, `instNormalSubtypeMemFocalAddSubgroupOf`, `map_focalAddSubgroupOf`, `commutator_inf_eq_focalSubgroup`, `commutator_le_focalSubgroup`, `commutator_le_focalSubgroupOf`, `mk'_conj_eq`, `pow_index_surjective`, `focalSubgroupOf_def`, `focalSubgroupOf_eq_closure`, `focalSubgroup_def`, `focalSubgroup_le`, `focalSubgroup_le_commutator`, `instIsMulCommutativeQuotientSubtypeMemFocalSubgroupOf`, `instNormalSubtypeMemFocalSubgroupOf`, `ker_restrict_transferFocal_eq_focalSubgroupOf`, `ker_transferFocal_inf_eq_focalSubgroup`, `map_focalSubgroupOf`, `transferFocal_eq_pow`, `transferFocal_surjective`	28
Total	35

AddSubgroup

Definitions

Name	Category	Theorems
`focalAddSubgroup` 📖	CompOp	6 math math: `focalAddSubgroup_le`, `map_focalAddSubgroupOf`, `addCommutator_le_focalAddSubgroup`, `focalAddSubgroup_le_addCommutator`, `focalAddSubgroupOf_def`, `focalAddSubgroup_def`
`focalAddSubgroupOf` 📖	CompOp	7 math math: `addCommutator_le_focalAddSubgroupOf`, `map_focalAddSubgroupOf`, `focalAddSubgroupOf_eq_closure`, `focalAddSubgroupOf_def`, `instIsAddCommutativeQuotientSubtypeMemFocalAddSubgroupOf`, `focalAddSubgroupOf.mk'_addConj_eq`, `instNormalSubtypeMemFocalAddSubgroupOf`
`transferFocal` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addCommutator_le_focalAddSubgroup` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `addCommutator` `focalAddSubgroup`	—	`map_subtype_addCommutator` `le_imp_le_of_le_of_le` `map_mono` `addCommutator_le_focalAddSubgroupOf` `le_refl` `map_focalAddSubgroupOf`
`addCommutator_le_focalAddSubgroupOf` 📖	mathematical	—	`AddSubgroup` `SetLike.instMembership` `instSetLike` `toAddGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `addCommutator` `focalAddSubgroupOf`	—	`focalAddSubgroupOf_eq_closure` `closure_mono`
`focalAddSubgroupOf_def` 📖	mathematical	—	`focalAddSubgroupOf` `addSubgroupOf` `focalAddSubgroup`	—	—
`focalAddSubgroupOf_eq_closure` 📖	mathematical	—	`focalAddSubgroupOf` `closure` `AddSubgroup` `SetLike.instMembership` `instSetLike` `toAddGroup` `setOf` `Bracket.bracket` `addCommutatorElement`	—	`map_focalAddSubgroupOf` `AddMonoidHom.map_closure` `focalAddSubgroup_def`
`focalAddSubgroup_def` 📖	mathematical	—	`focalAddSubgroup` `closure` `setOf` `AddSubgroup` `SetLike.instMembership` `instSetLike` `Bracket.bracket` `addCommutatorElement`	—	—
`focalAddSubgroup_le` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `focalAddSubgroup`	—	`focalAddSubgroup_def` `closure_le`
`focalAddSubgroup_le_addCommutator` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `focalAddSubgroup` `addCommutator`	—	`focalAddSubgroup_def` `closure_le` `addCommutator_mem_addCommutator` `mem_top`
`instIsAddCommutativeQuotientSubtypeMemFocalAddSubgroupOf` 📖	mathematical	—	`IsAddCommutative` `HasQuotient.Quotient` `AddSubgroup` `SetLike.instMembership` `instSetLike` `toAddGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `focalAddSubgroupOf` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `instNormalSubtypeMemFocalAddSubgroupOf`	—	`instNormalSubtypeMemFocalAddSubgroupOf` `Normal.quotient_commutative_iff_addCommutator_le` `addCommutator_le_focalAddSubgroupOf`
`instNormalSubtypeMemFocalAddSubgroupOf` 📖	mathematical	—	`Normal` `AddSubgroup` `SetLike.instMembership` `instSetLike` `toAddGroup` `focalAddSubgroupOf`	—	`focalAddSubgroupOf_def` `normal_addSubgroupOf_iff` `focalAddSubgroup_le` `closure_induction` `subset_closure` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass` `neg_mem_iff` `AddSubgroupClass.toNegMemClass` `neg_one_zsmul` `add_assoc` `Mathlib.Tactic.Group.zsmul_trick_zero'` `neg_add_cancel` `zero_zsmul` `add_zero` `neg_one_zsmul_add` `mul_zsmul'` `mul_one` `neg_neg` `one_zsmul` `add_neg_cancel` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `addConj_add` `neg_add_rev` `NegMemClass.neg_mem`
`map_focalAddSubgroupOf` 📖	mathematical	—	`map` `AddSubgroup` `SetLike.instMembership` `instSetLike` `toAddGroup` `subtype` `focalAddSubgroupOf` `focalAddSubgroup`	—	`map_addSubgroupOf_eq_of_le` `focalAddSubgroup_le`

AddSubgroup.focalAddSubgroupOf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk'_addConj_eq` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`DFunLike.coe` `AddMonoidHom` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `HasQuotient.Quotient` `AddSubgroup.toAddGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `AddSubgroup.focalAddSubgroupOf` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `AddSubgroup.instNormalSubtypeMemFocalAddSubgroupOf` `AddMonoidHom.instFunLike` `QuotientAddGroup.mk'` `AddZero.toAdd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`QuotientAddGroup.eq` `AddSubgroup.focalAddSubgroupOf_def` `AddSubgroup.mem_addSubgroupOf` `AddSubgroup.subset_closure` `AddSubgroup.add_mem` `AddSubgroup.neg_mem` `neg_one_zsmul` `neg_one_zsmul_add` `mul_zsmul'` `mul_one` `neg_neg` `one_zsmul` `add_assoc` `Mathlib.Tactic.Group.zsmul_trick_zero` `neg_add_cancel` `zero_zsmul` `add_zero`

Subgroup

Definitions

Name	Category	Theorems
`focalSubgroup` 📖	CompOp	8 math math: `map_focalSubgroupOf`, `focalSubgroupOf_def`, `commutator_le_focalSubgroup`, `commutator_inf_eq_focalSubgroup`, `focalSubgroup_le_commutator`, `focalSubgroup_def`, `ker_transferFocal_inf_eq_focalSubgroup`, `focalSubgroup_le`
`focalSubgroupOf` 📖	CompOp	12 math math: `map_focalSubgroupOf`, `instNormalSubtypeMemFocalSubgroupOf`, `focalSubgroupOf.pow_index_surjective`, `transferFocal_surjective`, `focalSubgroupOf_def`, `instIsMulCommutativeQuotientSubtypeMemFocalSubgroupOf`, `transferFocal_eq_pow`, `focalSubgroupOf_eq_closure`, `ker_restrict_transferFocal_eq_focalSubgroupOf`, `focalSubgroupOf.mk'_conj_eq`, `ker_transferFocal_inf_eq_focalSubgroup`, `commutator_le_focalSubgroupOf`
`transferFocal` 📖	CompOp	4 math math: `transferFocal_surjective`, `transferFocal_eq_pow`, `ker_restrict_transferFocal_eq_focalSubgroupOf`, `ker_transferFocal_inf_eq_focalSubgroup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commutator_inf_eq_focalSubgroup` 📖	mathematical	—	`Subgroup` `instMin` `commutator` `Sylow.toSubgroup` `focalSubgroup`	—	`le_antisymm` `le_trans` `instNormalSubtypeMemFocalSubgroupOf` `inf_le_inf_right` `Abelianization.commutator_subset_ker` `instIsMulCommutativeQuotientSubtypeMemFocalSubgroupOf` `Eq.le` `ker_transferFocal_inf_eq_focalSubgroup` `le_inf` `focalSubgroup_le_commutator` `focalSubgroup_le`
`commutator_le_focalSubgroup` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `commutator` `focalSubgroup`	—	`map_subtype_commutator` `le_imp_le_of_le_of_le` `map_mono` `commutator_le_focalSubgroupOf` `le_refl` `map_focalSubgroupOf`
`commutator_le_focalSubgroupOf` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `instSetLike` `toGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `commutator` `focalSubgroupOf`	—	`focalSubgroupOf_eq_closure` `closure_mono`
`focalSubgroupOf_def` 📖	mathematical	—	`focalSubgroupOf` `subgroupOf` `focalSubgroup`	—	—
`focalSubgroupOf_eq_closure` 📖	mathematical	—	`focalSubgroupOf` `closure` `Subgroup` `SetLike.instMembership` `instSetLike` `toGroup` `setOf` `Bracket.bracket` `commutatorElement`	—	`map_focalSubgroupOf` `MonoidHom.map_closure` `focalSubgroup_def`
`focalSubgroup_def` 📖	mathematical	—	`focalSubgroup` `closure` `setOf` `Subgroup` `SetLike.instMembership` `instSetLike` `Bracket.bracket` `commutatorElement`	—	—
`focalSubgroup_le` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `focalSubgroup`	—	`focalSubgroup_def` `closure_le`
`focalSubgroup_le_commutator` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `focalSubgroup` `commutator`	—	`focalSubgroup_def` `closure_le` `commutator_mem_commutator` `mem_top`
`instIsMulCommutativeQuotientSubtypeMemFocalSubgroupOf` 📖	mathematical	—	`IsMulCommutative` `HasQuotient.Quotient` `Subgroup` `SetLike.instMembership` `instSetLike` `toGroup` `QuotientGroup.instHasQuotientSubgroup` `focalSubgroupOf` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `QuotientGroup.Quotient.group` `instNormalSubtypeMemFocalSubgroupOf`	—	`instNormalSubtypeMemFocalSubgroupOf` `Normal.quotient_commutative_iff_commutator_le` `commutator_le_focalSubgroupOf`
`instNormalSubtypeMemFocalSubgroupOf` 📖	mathematical	—	`Normal` `Subgroup` `SetLike.instMembership` `instSetLike` `toGroup` `focalSubgroupOf`	—	`focalSubgroupOf_def` `normal_subgroupOf_iff` `focalSubgroup_le` `closure_induction` `subset_closure` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubgroupClass.toSubmonoidClass` `instSubgroupClass` `SubgroupClass.toInvMemClass` `Mathlib.Tactic.Group.zpow_trick_one'` `neg_add_cancel` `zpow_zero` `mul_one` `mul_zpow_neg_one` `neg_neg` `zpow_one` `mul_inv_cancel` `SubmonoidClass.toOneMemClass` `conj_mul` `mul_assoc` `mul_inv_rev` `inv_inv` `InvMemClass.inv_mem`
`ker_restrict_transferFocal_eq_focalSubgroupOf` 📖	mathematical	—	`MonoidHom.ker` `Sylow` `SetLike.instMembership` `Sylow.instSetLike` `SubgroupClass.toGroup` `Sylow.instSubgroupClass` `HasQuotient.Quotient` `Subgroup` `instSetLike` `Sylow.toSubgroup` `toGroup` `QuotientGroup.instHasQuotientSubgroup` `focalSubgroupOf` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `QuotientGroup.Quotient.group` `instNormalSubtypeMemFocalSubgroupOf` `MonoidHom.restrict` `SubgroupClass.toSubmonoidClass` `transferFocal`	—	`ext` `Sylow.instSubgroupClass` `instNormalSubtypeMemFocalSubgroupOf` `SubgroupClass.toSubmonoidClass` `IsPGroup.to_quotient` `Sylow.isPGroup'` `MonoidHom.mem_ker` `MonoidHom.restrict_apply` `transferFocal_eq_pow` `Sylow.not_dvd_index` `one_pow` `Equiv.apply_eq_iff_eq`
`ker_transferFocal_inf_eq_focalSubgroup` 📖	mathematical	—	`Subgroup` `instMin` `MonoidHom.ker` `HasQuotient.Quotient` `SetLike.instMembership` `instSetLike` `Sylow.toSubgroup` `toGroup` `QuotientGroup.instHasQuotientSubgroup` `focalSubgroupOf` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `QuotientGroup.Quotient.group` `instNormalSubtypeMemFocalSubgroupOf` `transferFocal` `focalSubgroup`	—	`instNormalSubtypeMemFocalSubgroupOf` `subgroupOf_map_subtype` `SubgroupClass.toSubmonoidClass` `instSubgroupClass` `MonoidHom.ker_restrict` `map_focalSubgroupOf` `ker_restrict_transferFocal_eq_focalSubgroupOf`
`map_focalSubgroupOf` 📖	mathematical	—	`map` `Subgroup` `SetLike.instMembership` `instSetLike` `toGroup` `subtype` `focalSubgroupOf` `focalSubgroup`	—	`map_subgroupOf_eq_of_le` `focalSubgroup_le`
`transferFocal_eq_pow` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `HasQuotient.Quotient` `Subgroup` `SetLike.instMembership` `instSetLike` `toGroup` `QuotientGroup.instHasQuotientSubgroup` `focalSubgroupOf` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `QuotientGroup.Quotient.group` `instNormalSubtypeMemFocalSubgroupOf` `MonoidHom.instFunLike` `transferFocal` `Monoid.toPow` `index`	—	`Quotient.finite` `finite_quotient_of_finiteIndex` `instNormalSubtypeMemFocalSubgroupOf` `instIsMulCommutativeQuotientSubtypeMemFocalSubgroupOf` `transferFocal.eq_1` `MulAction.left_quotientAction` `index_eq_sum_minimalPeriod` `Finset.prod_pow_eq_pow_sum` `QuotientGroup.out_conj_pow_minimalPeriod_mem` `MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot` `Finset.prod_congr` `focalSubgroupOf.mk'_conj_eq` `instSubgroupClass`
`transferFocal_surjective` 📖	mathematical	—	`HasQuotient.Quotient` `Subgroup` `SetLike.instMembership` `instSetLike` `Sylow.toSubgroup` `toGroup` `QuotientGroup.instHasQuotientSubgroup` `focalSubgroupOf` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `QuotientGroup.Quotient.group` `instNormalSubtypeMemFocalSubgroupOf` `MonoidHom.instFunLike` `transferFocal`	—	`instNormalSubtypeMemFocalSubgroupOf` `focalSubgroupOf.pow_index_surjective` `QuotientGroup.mk'_surjective` `transferFocal_eq_pow`

Subgroup.focalSubgroupOf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk'_conj_eq` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`DFunLike.coe` `MonoidHom` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `HasQuotient.Quotient` `Subgroup.toGroup` `QuotientGroup.instHasQuotientSubgroup` `Subgroup.focalSubgroupOf` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `QuotientGroup.Quotient.group` `Subgroup.instNormalSubtypeMemFocalSubgroupOf` `MonoidHom.instFunLike` `QuotientGroup.mk'` `MulOne.toMul` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`QuotientGroup.eq` `Subgroup.focalSubgroupOf_def` `Subgroup.mem_subgroupOf` `Subgroup.subset_closure` `Subgroup.mul_mem` `Subgroup.inv_mem` `mul_zpow_neg_one` `mul_one` `neg_neg` `zpow_one` `Mathlib.Tactic.Group.zpow_trick_one` `neg_add_cancel` `zpow_zero`
`pow_index_surjective` 📖	mathematical	—	`HasQuotient.Quotient` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Sylow.toSubgroup` `Subgroup.toGroup` `QuotientGroup.instHasQuotientSubgroup` `Subgroup.focalSubgroupOf` `Monoid.toPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `QuotientGroup.Quotient.group` `Subgroup.instNormalSubtypeMemFocalSubgroupOf` `Subgroup.index`	—	`Equiv.surjective` `Subgroup.instNormalSubtypeMemFocalSubgroupOf` `IsPGroup.to_quotient` `Sylow.isPGroup'` `Sylow.not_dvd_index`

Subgroup.transferFocal

Definitions

Name	Category	Theorems
`quotientKerMulEquivQuotientFocalSubroupOf` 📖	CompOp	—

---

← Back to Index