Documentation Verification Report

FiniteIndexNormalSubgroup

📁 Source: Mathlib/GroupTheory/FiniteIndexNormalSubgroup.lean

Statistics

Metric	Count
Definitions `FiniteIndexNormalAddSubgroup`, `comap`, `instCoeAddSubgroup`, `instInfFiniteIndexNormalAddSubgroup`, `instLattice`, `instMax`, `instPartialOrder`, `instPartialOrderFiniteIndexNormalAddSubgroup`, `instSemilatticeInfFiniteIndexNormalAddSubgroup`, `instSemilatticeSupFiniteIndexNormalAddSubgroup`, `instSetLike`, `ofAddSubgroup`, `toAddSubgroup`, `FiniteIndexNormalSubgroup`, `comap`, `instCoeSubgroup`, `instInfFiniteIndexNormalSubgroup`, `instLattice`, `instMax`, `instPartialOrder`, `instPartialOrderFiniteIndexNormalSubgroup`, `instSemilatticeInfFiniteIndexNormalSubgroup`, `instSemilatticeSupFiniteIndexNormalSubgroup`, `instSetLike`, `ofSubgroup`, `toSubgroup`	26
Theorems `comap_comp`, `comap_id`, `comap_mono`, `ext`, `ext_iff`, `instAddSubgroupClass`, `instFiniteIndex`, `instNormal`, `isFiniteIndex'`, `isNormal'`, `toAddSubgroup_comap`, `toAddSubgroup_injective`, `toAddSubgroup_ofAddSubgroup`, `comap_comp`, `comap_id`, `comap_mono`, `ext`, `ext_iff`, `instFiniteIndex`, `instNormal`, `instSubgroupClass`, `isFiniteIndex'`, `isNormal'`, `toSubgroup_comap`, `toSubgroup_injective`, `toSubgroup_ofSubgroup`	26
Total	52

FiniteIndexNormalAddSubgroup

Definitions

Name	Category	Theorems
`comap` 📖	CompOp	4 math math: `comap_mono`, `toAddSubgroup_comap`, `comap_comp`, `comap_id`
`instCoeAddSubgroup` 📖	CompOp	—
`instInfFiniteIndexNormalAddSubgroup` 📖	CompOp	—
`instLattice` 📖	CompOp	—
`instMax` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	—
`instPartialOrderFiniteIndexNormalAddSubgroup` 📖	CompOp	1 math math: `OpenNormalAddSubgroup.toFiniteIndexNormalAddSubgroup_mono`
`instSemilatticeInfFiniteIndexNormalAddSubgroup` 📖	CompOp	—
`instSemilatticeSupFiniteIndexNormalAddSubgroup` 📖	CompOp	—
`instSetLike` 📖	CompOp	1 math math: `instAddSubgroupClass`
`ofAddSubgroup` 📖	CompOp	1 math math: `toAddSubgroup_ofAddSubgroup`
`toAddSubgroup` 📖	CompOp	8 math math: `isFiniteIndex'`, `isNormal'`, `ext_iff`, `instNormal`, `toAddSubgroup_comap`, `instFiniteIndex`, `toAddSubgroup_injective`, `toAddSubgroup_ofAddSubgroup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_comp` 📖	mathematical	—	`comap` `AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—
`comap_id` 📖	mathematical	—	`comap` `AddMonoidHom.id` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—
`comap_mono` 📖	mathematical	`FiniteIndexNormalAddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderFiniteIndexNormalAddSubgroup`	`comap`	—	—
`ext` 📖	—	`AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubmonoid.toAddSubsemigroup` `AddSubgroup.toAddSubmonoid` `toAddSubgroup`	—	—	—
`ext_iff` 📖	mathematical	—	`AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubmonoid.toAddSubsemigroup` `AddSubgroup.toAddSubmonoid` `toAddSubgroup`	—	`ext`
`instAddSubgroupClass` 📖	mathematical	—	`AddSubgroupClass` `FiniteIndexNormalAddSubgroup` `AddGroup.toSubNegMonoid` `instSetLike`	—	`AddSubsemigroup.add_mem'` `AddSubmonoid.zero_mem'` `AddSubgroup.neg_mem'`
`instFiniteIndex` 📖	mathematical	—	`AddSubgroup.FiniteIndex` `toAddSubgroup`	—	`isFiniteIndex'`
`instNormal` 📖	mathematical	—	`AddSubgroup.Normal` `toAddSubgroup`	—	`isNormal'`
`isFiniteIndex'` 📖	mathematical	—	`AddSubgroup.FiniteIndex` `toAddSubgroup`	—	—
`isNormal'` 📖	mathematical	—	`AddSubgroup.Normal` `toAddSubgroup`	—	—
`toAddSubgroup_comap` 📖	mathematical	—	`toAddSubgroup` `comap` `AddSubgroup.comap`	—	—
`toAddSubgroup_injective` 📖	mathematical	—	`FiniteIndexNormalAddSubgroup` `AddSubgroup` `toAddSubgroup`	—	`ext` `Set.ext`
`toAddSubgroup_ofAddSubgroup` 📖	mathematical	—	`toAddSubgroup` `ofAddSubgroup`	—	—

FiniteIndexNormalSubgroup

Definitions

Name	Category	Theorems
`comap` 📖	CompOp	4 math math: `comap_comp`, `comap_mono`, `comap_id`, `toSubgroup_comap`
`instCoeSubgroup` 📖	CompOp	—
`instInfFiniteIndexNormalSubgroup` 📖	CompOp	—
`instLattice` 📖	CompOp	—
`instMax` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	—
`instPartialOrderFiniteIndexNormalSubgroup` 📖	CompOp	2 math math: `ProfiniteGrp.ProfiniteCompletion.preimage_le`, `OpenNormalSubgroup.toFiniteIndexNormalSubgroup_mono`
`instSemilatticeInfFiniteIndexNormalSubgroup` 📖	CompOp	—
`instSemilatticeSupFiniteIndexNormalSubgroup` 📖	CompOp	—
`instSetLike` 📖	CompOp	1 math math: `instSubgroupClass`
`ofSubgroup` 📖	CompOp	1 math math: `toSubgroup_ofSubgroup`
`toSubgroup` 📖	CompOp	8 math math: `toSubgroup_ofSubgroup`, `instFiniteIndex`, `ext_iff`, `instNormal`, `isFiniteIndex'`, `toSubgroup_injective`, `isNormal'`, `toSubgroup_comap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_comp` 📖	mathematical	—	`comap` `MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`comap_id` 📖	mathematical	—	`comap` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`comap_mono` 📖	mathematical	`FiniteIndexNormalSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderFiniteIndexNormalSubgroup`	`comap`	—	—
`ext` 📖	—	`Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Submonoid.toSubsemigroup` `Subgroup.toSubmonoid` `toSubgroup`	—	—	—
`ext_iff` 📖	mathematical	—	`Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Submonoid.toSubsemigroup` `Subgroup.toSubmonoid` `toSubgroup`	—	`ext`
`instFiniteIndex` 📖	mathematical	—	`Subgroup.FiniteIndex` `toSubgroup`	—	`isFiniteIndex'`
`instNormal` 📖	mathematical	—	`Subgroup.Normal` `toSubgroup`	—	`isNormal'`
`instSubgroupClass` 📖	mathematical	—	`SubgroupClass` `FiniteIndexNormalSubgroup` `Group.toDivInvMonoid` `instSetLike`	—	`Subsemigroup.mul_mem'` `Submonoid.one_mem'` `Subgroup.inv_mem'`
`isFiniteIndex'` 📖	mathematical	—	`Subgroup.FiniteIndex` `toSubgroup`	—	—
`isNormal'` 📖	mathematical	—	`Subgroup.Normal` `toSubgroup`	—	—
`toSubgroup_comap` 📖	mathematical	—	`toSubgroup` `comap` `Subgroup.comap`	—	—
`toSubgroup_injective` 📖	mathematical	—	`FiniteIndexNormalSubgroup` `Subgroup` `toSubgroup`	—	`ext` `Set.ext`
`toSubgroup_ofSubgroup` 📖	mathematical	—	`toSubgroup` `ofSubgroup`	—	—

(root)

Definitions

Name	Category	Theorems
`FiniteIndexNormalAddSubgroup` 📖	CompData	4 math math: `OpenNormalAddSubgroup.toFiniteIndexNormalAddSubgroup_injective`, `FiniteIndexNormalAddSubgroup.instAddSubgroupClass`, `OpenNormalAddSubgroup.toFiniteIndexNormalAddSubgroup_mono`, `FiniteIndexNormalAddSubgroup.toAddSubgroup_injective`
`FiniteIndexNormalSubgroup` 📖	CompData	5 math math: `FiniteIndexNormalSubgroup.instSubgroupClass`, `ProfiniteGrp.ProfiniteCompletion.preimage_le`, `FiniteIndexNormalSubgroup.toSubgroup_injective`, `OpenNormalSubgroup.toFiniteIndexNormalSubgroup_injective`, `OpenNormalSubgroup.toFiniteIndexNormalSubgroup_mono`

---

← Back to Index