Documentation Verification Report

ResiduallyFinite

📁 Source: Mathlib/GroupTheory/ResiduallyFinite.lean

Statistics

Metric	Count
Definitions `ResiduallyFinite`, `ResiduallyFinite`	2
Theorems `iInf_eq_bot`, `eq_zero_iff_forall_finiteIndexNormalSubroup`, `instResiduallyFiniteOfFinite`, `residuallyFinite_def`, `residuallyFinite_iff_exists_finiteIndex`, `residuallyFinite_iff_exists_finiteIndexNormalAddSubgroup`, `residuallyFinite_iff_forall_finiteIndex`, `residuallyFinite_iff_forall_finiteIndexNormalAddSubgroup`, `iInf_eq_bot`, `eq_one_iff_forall_finiteIndexNormalSubroup`, `instResiduallyFiniteOfFinite`, `residuallyFinite_def`, `residuallyFinite_iff_exists_finiteIndex`, `residuallyFinite_iff_exists_finiteIndexNormalSubgroup`, `residuallyFinite_iff_forall_finiteIndex`, `residuallyFinite_iff_forall_finiteIndexNormalSubgroup`	16
Total	18

AddGroup

Definitions

Name	Category	Theorems
`ResiduallyFinite` 📖	CompData	6 math math: `residuallyFinite_iff_exists_finiteIndexNormalAddSubgroup`, `residuallyFinite_def`, `instResiduallyFiniteOfFinite`, `residuallyFinite_iff_forall_finiteIndexNormalAddSubgroup`, `residuallyFinite_iff_exists_finiteIndex`, `residuallyFinite_iff_forall_finiteIndex`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_zero_iff_forall_finiteIndexNormalSubroup` 📖	mathematical	`FiniteIndexNormalAddSubgroup` `SetLike.instMembership` `FiniteIndexNormalAddSubgroup.instSetLike`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `toSubtractionMonoid`	—	`residuallyFinite_iff_forall_finiteIndexNormalAddSubgroup`
`instResiduallyFiniteOfFinite` 📖	mathematical	—	`ResiduallyFinite`	—	`residuallyFinite_iff_forall_finiteIndex` `AddSubgroup.finiteIndex_of_finite`
`residuallyFinite_def` 📖	mathematical	—	`ResiduallyFinite` `iInf` `AddSubgroup` `FiniteIndexNormalAddSubgroup` `AddSubgroup.instInfSet` `FiniteIndexNormalAddSubgroup.toAddSubgroup` `Bot.bot` `AddSubgroup.instBot`	—	`ResiduallyFinite.iInf_eq_bot`
`residuallyFinite_iff_exists_finiteIndex` 📖	mathematical	—	`ResiduallyFinite` `AddSubgroup` `AddSubgroup.FiniteIndex` `SetLike.instMembership` `AddSubgroup.instSetLike`	—	`residuallyFinite_iff_forall_finiteIndex` `not_imp_not`
`residuallyFinite_iff_exists_finiteIndexNormalAddSubgroup` 📖	mathematical	—	`ResiduallyFinite` `FiniteIndexNormalAddSubgroup` `SetLike.instMembership` `FiniteIndexNormalAddSubgroup.instSetLike`	—	`residuallyFinite_iff_forall_finiteIndexNormalAddSubgroup` `not_imp_not`
`residuallyFinite_iff_forall_finiteIndex` 📖	mathematical	—	`ResiduallyFinite` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `toSubtractionMonoid`	—	`residuallyFinite_iff_forall_finiteIndexNormalAddSubgroup` `FiniteIndexNormalAddSubgroup.instFiniteIndex` `AddSubgroup.normalCore_le` `AddSubgroup.normalCore_normal` `AddSubgroup.finiteIndex_normalCore`
`residuallyFinite_iff_forall_finiteIndexNormalAddSubgroup` 📖	mathematical	—	`ResiduallyFinite` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `toSubtractionMonoid`	—	`residuallyFinite_def` `AddSubgroup.eq_bot_iff_forall` `AddSubgroup.mem_iInf` `FiniteIndexNormalAddSubgroup.mem_toAddSubgroup_iff`

AddGroup.ResiduallyFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iInf_eq_bot` 📖	mathematical	—	`iInf` `AddSubgroup` `FiniteIndexNormalAddSubgroup` `AddSubgroup.instInfSet` `FiniteIndexNormalAddSubgroup.toAddSubgroup` `Bot.bot` `AddSubgroup.instBot`	—	—

Group

Definitions

Name	Category	Theorems
`ResiduallyFinite` 📖	CompData	8 math math: `instResiduallyFiniteOfFinite`, `residuallyFinite_iff_forall_finiteIndex`, `residuallyFinite_iff_forall_finiteIndexNormalSubgroup`, `ProfiniteGrp.ProfiniteCompletion.etaFn_injective_iff_residuallyFinite`, `residuallyFinite_def`, `ProfiniteGrp.ProfiniteCompletion.mono_eta_iff_residuallyFinite`, `residuallyFinite_iff_exists_finiteIndexNormalSubgroup`, `residuallyFinite_iff_exists_finiteIndex`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_one_iff_forall_finiteIndexNormalSubroup` 📖	mathematical	`FiniteIndexNormalSubgroup` `SetLike.instMembership` `FiniteIndexNormalSubgroup.instSetLike`	`InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `toDivisionMonoid`	—	`residuallyFinite_iff_forall_finiteIndexNormalSubgroup`
`instResiduallyFiniteOfFinite` 📖	mathematical	—	`ResiduallyFinite`	—	`residuallyFinite_iff_forall_finiteIndex` `Subgroup.finiteIndex_of_finite`
`residuallyFinite_def` 📖	mathematical	—	`ResiduallyFinite` `iInf` `Subgroup` `FiniteIndexNormalSubgroup` `Subgroup.instInfSet` `FiniteIndexNormalSubgroup.toSubgroup` `Bot.bot` `Subgroup.instBot`	—	`ResiduallyFinite.iInf_eq_bot`
`residuallyFinite_iff_exists_finiteIndex` 📖	mathematical	—	`ResiduallyFinite` `Subgroup` `Subgroup.FiniteIndex` `SetLike.instMembership` `Subgroup.instSetLike`	—	—
`residuallyFinite_iff_exists_finiteIndexNormalSubgroup` 📖	mathematical	—	`ResiduallyFinite` `FiniteIndexNormalSubgroup` `SetLike.instMembership` `FiniteIndexNormalSubgroup.instSetLike`	—	—
`residuallyFinite_iff_forall_finiteIndex` 📖	mathematical	—	`ResiduallyFinite` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `toDivisionMonoid`	—	`residuallyFinite_iff_forall_finiteIndexNormalSubgroup` `FiniteIndexNormalSubgroup.instFiniteIndex` `Subgroup.normalCore_le` `Subgroup.normalCore_normal` `Subgroup.finiteIndex_normalCore`
`residuallyFinite_iff_forall_finiteIndexNormalSubgroup` 📖	mathematical	—	`ResiduallyFinite` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `toDivisionMonoid`	—	—

Group.ResiduallyFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iInf_eq_bot` 📖	mathematical	—	`iInf` `Subgroup` `FiniteIndexNormalSubgroup` `Subgroup.instInfSet` `FiniteIndexNormalSubgroup.toSubgroup` `Bot.bot` `Subgroup.instBot`	—	—

---

← Back to Index