Documentation Verification Report

Cofinite

📁 Source: Mathlib/RingTheory/Finiteness/Cofinite.lean

Statistics

Metric	Count
Definitions `CoFG`	1
Theorems `iff_cofg_bot`, `fg_of_isCompl`, `inf`, `ker`, `of_cofg_le`, `of_finite`, `sInf`, `sInf_of_finite`, `top`, `cofg_of_isCompl`, `range_fg_iff_ker_cofg`	11
Total	12

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_cofg_bot` 📖	mathematical	—	`Submodule.CoFG` `Bot.bot` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instBot` `Module.Finite`	—	`equiv` `Submodule.CoFG.of_finite`

Submodule

Definitions

Name	Category	Theorems
`CoFG` 📖	MathDef	8 math math: `FG.cofg_of_isCompl`, `CoFG.of_cofg_le`, `range_fg_iff_ker_cofg`, `CoFG.of_finite`, `CoFG.ker`, `CoFG.top`, `CoFG.inf`, `Module.Finite.iff_cofg_bot`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`range_fg_iff_ker_cofg` 📖	mathematical	—	`FG` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `CoFG` `LinearMap.ker`	—	`RingHomSurjective.ids` `Module.Finite.iff_fg` `Module.Finite.equiv_iff` `RingHomInvPair.ids`

Submodule.CoFG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg_of_isCompl` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`Submodule.FG`	—	`Module.Finite.iff_fg` `Module.Finite.equiv`
`inf` 📖	mathematical	—	`Submodule.CoFG` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instMin`	—	`Submodule.ker_mkQ` `LinearMap.ker_prod` `ker` `isNoetherian_prod` `isNoetherian_of_isNoetherianRing_of_finite`
`ker` 📖	mathematical	—	`Submodule.CoFG` `LinearMap.ker` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`RingHomSurjective.ids` `Submodule.range_fg_iff_ker_cofg` `IsNoetherian.noetherian`
`of_cofg_le` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	`Submodule.CoFG`	—	`sup_eq_right` `Module.Finite.equiv` `RingHomSurjective.ids` `Module.Finite.quotient`
`of_finite` 📖	mathematical	—	`Submodule.CoFG`	—	`Module.Finite.quotient` `IsScalarTower.left`
`sInf` 📖	mathematical	`Submodule.CoFG`	`InfSet.sInf` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instInfSet` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Finset.induction` `Finset.coe_empty` `sInf_empty` `Finset.coe_insert` `sInf_insert` `inf`
`sInf_of_finite` 📖	mathematical	`Submodule.CoFG`	`InfSet.sInf` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instInfSet`	—	`Set.Finite.coe_toFinset` `sInf`
`top` 📖	mathematical	—	`Submodule.CoFG` `Top.top` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instTop`	—	`Module.IsNoetherian.finite` `isNoetherian_of_finite` `Finite.of_fintype`

Submodule.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cofg_of_isCompl` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `Submodule.FG`	`Submodule.CoFG`	—	`Module.Finite.equiv` `Module.Finite.iff_fg` `RingHomInvPair.ids` `IsCompl.symm`

---

← Back to Index