Small

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

Statistics

Metric	Count
Definitions Small, instInhabitedSubtypeSmallMem, instSemilatticeSupSubtypeSmallMem	3
Theorems small, small_adjoin, small, small, small, small_iSup, small_span, small_span_singleton, small_sup	9
Total	12

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
small_adjoin 📖	mathematical	—	Small Subalgebra CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike adjoin	—	adjoin_eq_range small_range MvPolynomial.instSmall

Algebra.FiniteType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
small 📖	mathematical	—	Small	—	Subalgebra.FG.small out small_univ_iff

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
small 📖	mathematical	—	Small	—	Submodule.FG.small Module.finite_def small_univ_iff

Subalgebra.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
small 📖	mathematical	Subalgebra.FG CommSemiring.toSemiring	Small Subalgebra CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike	—	Algebra.small_adjoin Countable.toSmall Finite.to_countable Finite.of_fintype

Submodule

Definitions

Name	Category	Theorems
instInhabitedSubtypeSmallMem 📖	CompOp	—
instSemilatticeSupSubtypeSmallMem 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
small_iSup 📖	mathematical	Small Submodule SetLike.instMembership setLike	Small Submodule SetLike.instMembership setLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	RingHomSurjective.ids RingHomInvPair.ids AddMonoid.nat_smulCommClass' iSup_eq_range_dfinsupp_lsum small_range DFinsupp.small
small_span 📖	mathematical	—	Small Submodule SetLike.instMembership setLike span	—	Set.iUnion_singleton_eq_range Subtype.range_coe_subtype small_iSup small_span_singleton
small_span_singleton 📖	mathematical	—	Small Submodule SetLike.instMembership setLike span Set Set.instSingletonSet	—	FG.small fg_span_singleton
small_sup 📖	mathematical	—	Small Submodule SetLike.instMembership setLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice	—	RingHomSurjective.ids sup_eq_range small_range small_prod

Submodule.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
small 📖	mathematical	Submodule.FG	Small Submodule SetLike.instMembership Submodule.setLike	—	Submodule.fg_iff_exists_fin_generating_family RingHomSurjective.ids Fintype.range_linearCombination small_range small_Pi UnivLE.small univLE_of_max UnivLE.self

(root)

Definitions

Name	Category	Theorems
Small 📖	CompData	171 math math: CategoryTheory.OrthogonalReflection.instSmallD₂, small_congr, small_sum, small_union, TensorProduct.instSmall, small_biUnion, small_biInter, instSmallUnitsSkeletonModuleCat, CommGrpCat.hasLimit_iff_small_sections, ModuleCat.instSmallSubtypeForallCarrierObjMemSubmoduleSectionsSubmodule, small_max, FirstOrder.Language.Substructure.small_closure, small_iInter', MvPolynomial.instSmall, small_inter_of_left, AddCommGrpCat.instSmallQuot, CategoryTheory.instSmallHomOfLocallySmall, small_empty, Opposite.small, Finsupp.small, FirstOrder.Language.Substructure.small_bot, small_sigma, small_subsingleton, Small.mk', small_set_zero, CategoryTheory.IsCofiltered.small_fullSubcategory_cofilteredClosure, CategoryTheory.Localization.small_of_hasSmallLocalizedHom, not_small_ordinal, Cardinal.small_Iio, ZFSet.coeEquiv_apply_coe, CategoryTheory.Limits.Types.small_colimitType_of_hasColimit, small_sub, CategoryTheory.essentiallySmall_iff, not_small_type, small_setPi, CommMonCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections, small_image, small_quot, small_of_injective, SheafOfModules.instSmallElemForallObjCompModuleCatCarrierOppositeRingCatObjFunctorIsSheafPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections, CategoryTheory.small_of_small_arrow, FirstOrder.Language.Term.small, not_small_cardinal, small_of_surjective, HasCardinalLT.small, Cardinal.small_Icc, small_prod, small_single, small_subtype, CategoryTheory.InitiallySmall.exists_small_weakly_initial_set, instSmallLocalizedModule, TopCat.hasLimit_iff_small_sections, small_sInter, CategoryTheory.hasExt_iff_small_ext, UnivLE.small, Submodule.small_span_singleton, Ordinal.small_Iic, univLE_iff, CategoryTheory.SmallObject.instSmallιAttachCellsιFunctorObj, small_type, Algebra.FiniteType.small, small_sep, AddGrpCat.hasLimit_iff_small_sections, smallVector, Cardinal.small_Ioo, CategoryTheory.ObjectProperty.instSmallFullSubcategoryOfSmall, GrpCat.hasLimit_iff_small_sections, small_of_injective_of_exists, small_image2, small_inter_of_right, CategoryTheory.WellPowered.subobject_small, CategoryTheory.instSmallCarrierObjOppositeMonCatMonFunctorYonedaMon, small_pair, CategoryTheory.Limits.Types.hasColimit_iff_small_colimitType, Cardinal.small_Ioc, AddCommMonCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections, small_mul, TopCat.hasColimit_iff_small_colimitType, small_iUnion, Submodule.Quotient.instSmallQuotient, small_div, Algebra.small_adjoin, CategoryTheory.instSmallDiscrete, small_setProd, CategoryTheory.instSmallFunctorOfLocallySmall, CategoryTheory.small_skeleton_of_essentiallySmall, CategoryTheory.small_subobject, Ordinal.bddAbove_iff_small, small_succ, Small.trans_univLE, CategoryTheory.LocallySmall.hom_small, Manifold.IsImmersionAtOfComplement.small, small_insert, FirstOrder.Language.Theory.ModelType.of_small, small_Pi, small_diff, CategoryTheory.instSmallHomDerivedCategoryObjSingleFunctorOfHasExt, Ordinal.small_Icc, small_iff, GrpCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections, DFinsupp.small, small_univ, Submodule.small_iSup, CategoryTheory.FinallySmall.exists_small_weakly_terminal_set, small_sInter', CategoryTheory.SmallObject.instSmallFunctorObjIndex, CategoryTheory.instSmallArrowOfLocallySmall, AddGrpCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections, Cardinal.small_iff_lift_mk_lt_univ, small_ulift, small_self, CategoryTheory.IsFiltered.small_fullSubcategory_filteredClosure, CategoryTheory.instSmallCarrierObjOppositeGrpCatGrpFunctorYonedaGrp, Ordinal.small_Ioc, smallList, Cardinal.small_Iic, Cardinal.bddAbove_iff_small, CategoryTheory.Localization.hasSmallLocalizedHom_iff, CategoryTheory.initiallySmall_iff_exists_small_weakly_initial_set, small_subset, AlgCat.instSmallSubtypeForallCarrierObjMemSubalgebraSectionsSubalgebra, FirstOrder.Language.exists_small_elementarySubstructure, Module.Finite.small, small_set_one, small_set, CategoryTheory.Limits.Concrete.small_sections_of_hasLimit, CategoryTheory.OrthogonalReflection.instSmallLMultispanShape, small_zero, CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR, CategoryTheory.CostructuredArrow.instSmallOfLocallySmall, Submodule.small_span, CategoryTheory.MorphismProperty.IsSmall.small_toSet, CategoryTheory.Limits.Types.hasLimit_iff_small_sections, Subalgebra.FG.small, small_map, small_sUnion, Ordinal.small_Ioo, Cardinal.small_Ico, FirstOrder.Language.Substructure.elementarySkolem₁Reduct.instSmall, small_neg, Ordinal.small_Iio, CategoryTheory.hasExt_iff, small_range, ZFSet.small_toSet, CategoryTheory.Localization.hasSmallLocalizedShiftedHom_iff, Submodule.FG.small, CategoryTheory.instSmallHomFunctorOppositeTypeColimitCompYoneda, small_quotient, CategoryTheory.Functor.instSmallColimitType, Countable.toSmall, CategoryTheory.finallySmall_iff_exists_small_weakly_terminal_set, small_plift, CategoryTheory.StructuredArrow.instSmallOfLocallySmall, small_univ_iff, LightCondensed.instSmallHom, CategoryTheory.Localization.HasSmallLocalizedHom.small, small_iInter, small_add, ZFSet.small_coe, Ordinal.small_Ico, FirstOrder.Language.ElementarySubstructure.toModel.instSmall, small_biInter', small_lift, Submodule.small_sup, small_powerset, AddCommGrpCat.hasColimit_iff_small_quot, AddCommGrpCat.hasLimit_iff_small_sections, CategoryTheory.OrthogonalReflection.instSmallD₁OfIsSmallOfLocallySmall, instSmallUnitsSkeletonSemimoduleCat, CategoryTheory.essentiallySmall_monoOver_iff_small_subobject, CategoryTheory.essentiallySmall_iff_of_thin

---

← Back to Index