Documentation Verification Report

FiniteLength

📁 Source: Mathlib/RingTheory/FiniteLength.lean

Statistics

Metric	Count
Definitions `IsFiniteLength`	1
Theorems `of_injective`, `of_surjective`, `finite_tfae`, `isFiniteLength`, `exists_compositionSeries_of_isNoetherian_isArtinian`, `instIsArtinianOfIsSemisimpleModuleOfFinite`, `isFiniteLength_iff_exists_compositionSeries`, `isFiniteLength_iff_isNoetherian_isArtinian`, `isFiniteLength_of_exists_compositionSeries`	9
Total	10

IsFiniteLength

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_injective` 📖	—	`IsFiniteLength` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	—	—	`isFiniteLength_iff_isNoetherian_isArtinian` `isNoetherian_of_injective` `isArtinian_of_injective`
`of_surjective` 📖	—	`IsFiniteLength` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	—	—	`isFiniteLength_iff_isNoetherian_isArtinian` `isNoetherian_of_surjective` `RingHomSurjective.ids` `LinearMap.range_eq_top` `isArtinian_of_surjective`

IsSemisimpleModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_tfae` 📖	mathematical	—	`List.TFAE` `Module.Finite` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `IsNoetherian` `IsArtinian` `IsFiniteLength` `Set` `Submodule` `Set.Finite` `sSupIndep` `Submodule.completeLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Top.top` `Submodule.instTop`	—	`isFiniteLength_iff_isNoetherian_isArtinian` `exists_sSupIndep_sSup_simples_eq_top` `instIsNoetherianOfFinite` `Module.IsNoetherian.finite` `WellFoundedGT.finite_of_sSupIndep` `wellFoundedGT` `WellFoundedLT.finite_of_sSupIndep` `isNoetherian_top_iff` `LinearEquiv.isArtinian_iff` `sSup_eq_iSup` `iSup_subtype''` `Set.Finite.to_subtype` `isNoetherian_iSup` `IsSimpleModule.instIsNoetherian` `SetCoe.forall'` `isArtinian_iSup` `Finite.to_wellFoundedLT` `IsSimpleOrder.instFinite` `IsSimpleModule.toIsSimpleOrder` `List.tfae_of_cycle`

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isFiniteLength` 📖	—	`IsFiniteLength`	—	—	`RingHomInvPair.ids` `Equiv.subsingleton` `RingHomSurjective.ids` `IsSimpleModule.congr` `RingHomSurjective.invPair`

(root)

Definitions

Name	Category	Theorems
`IsFiniteLength` 📖	CompData	8 math math: `isFiniteLength_of_exists_compositionSeries`, `isFiniteLength_iff_exists_compositionSeries`, `isFiniteLength_quotient_span_singleton`, `Module.length_ne_top_iff`, `IsSemisimpleModule.finite_tfae`, `IsArtinianRing.tfae`, `isArtinianRing_iff_isFiniteLength`, `isFiniteLength_iff_isNoetherian_isArtinian`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_compositionSeries_of_isNoetherian_isArtinian` 📖	mathematical	—	`RelSeries.head` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `setOf` `JordanHolderLattice.IsMaximal` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `JordanHolderModule.instJordanHolderLattice` `Bot.bot` `Submodule.instBot` `RelSeries.last` `Top.top` `Submodule.instTop`	—	`exists_covBy_seq_of_wellFoundedLT_wellFoundedGT` `wellFoundedGT` `IsMin.eq_bot` `IsMax.eq_top`
`instIsArtinianOfIsSemisimpleModuleOfFinite` 📖	mathematical	—	`IsArtinian` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`List.TFAE.out` `IsSemisimpleModule.finite_tfae`
`isFiniteLength_iff_exists_compositionSeries` 📖	mathematical	—	`IsFiniteLength` `RelSeries.head` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `setOf` `JordanHolderLattice.IsMaximal` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `JordanHolderModule.instJordanHolderLattice` `Bot.bot` `Submodule.instBot` `RelSeries.last` `Top.top` `Submodule.instTop`	—	`isFiniteLength_iff_isNoetherian_isArtinian` `exists_compositionSeries_of_isNoetherian_isArtinian` `isFiniteLength_of_exists_compositionSeries`
`isFiniteLength_iff_isNoetherian_isArtinian` 📖	mathematical	—	`IsFiniteLength` `IsNoetherian` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `IsArtinian`	—	`isNoetherian_of_finite` `Finite.of_subsingleton` `Finite.to_wellFoundedLT` `Finite.of_fintype` `isNoetherian_iff_submodule_quotient` `isNoetherian_iff'` `wellFoundedGT` `IsSimpleModule.instIsNoetherian` `isArtinian_iff_submodule_quotient` `IsSimpleOrder.instFinite` `IsSimpleModule.toIsSimpleOrder` `isFiniteLength_of_exists_compositionSeries` `exists_compositionSeries_of_isNoetherian_isArtinian`
`isFiniteLength_of_exists_compositionSeries` 📖	mathematical	`RelSeries.head` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `setOf` `JordanHolderLattice.IsMaximal` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `JordanHolderModule.instJordanHolderLattice` `Bot.bot` `Submodule.instBot` `RelSeries.last` `Top.top` `Submodule.instTop`	`IsFiniteLength`	—	`LinearEquiv.isFiniteLength` `Unique.instSubsingleton` `RelSeries.step` `covBy_iff_quot_is_simple` `CovBy.le` `RingHomInvPair.ids` `RingHomSurjective.invPair` `Submodule.injective_subtype` `inf_of_le_right` `RingHomSurjective.ids` `Submodule.map_comap_subtype`

---

← Back to Index