Documentation Verification Report

IsFinite

📁 Source: Mathlib/Algebra/Category/Grp/IsFinite.lean

Statistics

Metric	Count
Definitions `isFinite`, `IsFinite`, `IsFinite`, `IsFinite`, `IsFinite`, `IsFinite`	6
Theorems `instIsSerreClassIsFinite`, `prop_isFinite_iff`	2
Total	8

AddCommGrpCat

Definitions

Name	Category	Theorems
`isFinite` 📖	CompOp	2 math math: `prop_isFinite_iff`, `instIsSerreClassIsFinite`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsSerreClassIsFinite` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsSerreClass` `AddCommGrpCat` `instCategory` `instAbelian` `isFinite`	—	`isZero_of_subsingleton` `prop_isFinite_iff` `Finite.of_fintype` `Finite.of_injective` `mono_iff_injective` `Finite.of_surjective` `epi_iff_surjective` `CategoryTheory.ShortComplex.ShortExact.epi_g` `Function.Surjective.hasRightInverse` `CategoryTheory.ShortComplex.ab_exact_iff` `CategoryTheory.ShortComplex.ShortExact.exact` `map_sub` `AddMonoidHom.instAddMonoidHomClass` `sub_self` `sub_add_cancel` `Finite.instProd`
`prop_isFinite_iff` 📖	mathematical	—	`isFinite` `Finite` `carrier`	—	—

AlgebraicGeometry

Definitions

Name	Category	Theorems
`IsFinite` 📖	CompData	33 math math: `IsFinite.of_isProper_of_locallyQuasiFinite`, `IsFinite.instMorphismRestrict`, `instIsFiniteFiberToSpecResidueFieldOfLocallyQuasiFiniteOfQuasiCompact`, `IsFinite.comp_iff`, `IsFinite.iff_isProper_and_isAffineHom`, `IsFinite.instOfIsIsoScheme`, `IsFinite.instIsStableUnderBaseChangeScheme`, `IsFinite.eq_proper_inf_locallyQuasiFinite`, `locallyQuasiFinite_iff_isFinite_fiber`, `IsFinite.instCompScheme`, `IsFinite.instDescScheme`, `IsFinite.instFstScheme`, `IsFinite.instOfIsClosedImmersion`, `IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop`, `IsClosedImmersion.iff_isFinite_and_mono`, `IsFinite.instSndScheme`, `isFinite_iff_locallyOfFiniteType_of_jacobsonSpace`, `IsFinite.instIsMultiplicativeScheme`, `IsFinite.SpecMap_iff`, `IsFinite.iff_isProper_and_locallyQuasiFinite`, `IsClosedImmersion.eq_isFinite_inf_mono`, `IsFinite.eq_isProper_inf_isAffineHom`, `exists_isFinite_morphismRestrict_of_finite_preimage_singleton`, `isFinite_iff`, `IsFinite.of_locallyQuasiFinite`, `IsFinite.instIsStableUnderCompositionScheme`, `IsFinite.iff_isIntegralHom_and_locallyOfFiniteType`, `IsFinite.eq_inf`, `exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage`, `IsFinite.instContainsIdentitiesScheme`, `IsFinite.instHasOfPostcompPropertySchemeIsSeparated`, `IsFinite.of_comp`, `exists_etale_isCompl_of_quasiFiniteAt`

CategoryTheory.Subfunctor

Definitions

Name	Category	Theorems
`IsFinite` 📖	CompData	5 math math: `image_isFinite`, `Subpresheaf.IsGeneratedBy.isFinite`, `Subpresheaf.image_isFinite`, `range_isFinite`, `IsGeneratedBy.isFinite`

CategoryTheory.Subfunctor.Subpresheaf

Definitions

Name	Category	Theorems
`IsFinite` 📖	MathDef	—

SheafOfModules.Presentation

Definitions

Name	Category	Theorems
`IsFinite` 📖	CompData	1 math math: `SheafOfModules.QuasicoherentData.IsFinitePresentation.isFinite_presentation`

Stream'.WSeq

Definitions

Name	Category	Theorems
`IsFinite` 📖	CompData	—

---

← Back to Index