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 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	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	168 math math: Nimber.instSmallElemInvSet, not_small_nimber, CategoryTheory.OrthogonalReflection.instSmallD₂, small_congr, small_sum, small_union, TensorProduct.instSmall, small_biInter, instSmallUnitsSkeletonModuleCat, CommGrpCat.hasLimit_iff_small_sections, ModuleCat.instSmallSubtypeForallCarrierObjMemSubmoduleSectionsSubmodule, small_max, FirstOrder.Language.Substructure.small_closure, MvPolynomial.instSmall, small_inter_of_left, AddCommGrpCat.instSmallQuot, CategoryTheory.instSmallHomOfLocallySmall, small_empty, Opposite.small, Finsupp.small, FirstOrder.Language.Substructure.small_bot, 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, CommMonCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections, small_image, small_quot, small_of_injective, 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, 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, Nimber.small_Ioo, 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, small_pair, CategoryTheory.Limits.Types.hasColimit_iff_small_colimitType, Cardinal.small_Ioc, AddCommMonCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections, small_mul, TopCat.hasColimit_iff_small_colimitType, 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_diff, CategoryTheory.instSmallHomDerivedCategoryObjSingleFunctorOfHasExt, Ordinal.small_Icc, small_iff, Nimber.small_Ioc, GrpCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections, small_univ, Nimber.small_Icc, CategoryTheory.SmallObject.instSmallFunctorObjIndex, CategoryTheory.instSmallArrowOfLocallySmall, AddGrpCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections, Cardinal.small_iff_lift_mk_lt_univ, small_ulift, small_self, CategoryTheory.IsFiltered.small_fullSubcategory_filteredClosure, Ordinal.small_Ioc, Nimber.small_Iic, smallList, Cardinal.small_Iic, Cardinal.bddAbove_iff_small, CategoryTheory.Localization.hasSmallLocalizedHom_iff, small_subset, AlgCat.instSmallSubtypeForallCarrierObjMemSubalgebraSectionsSubalgebra, FirstOrder.Language.exists_small_elementarySubstructure, SetTheory.Game.small_setOf_birthday_lt, Module.Finite.small, small_set_one, small_set, CategoryTheory.Limits.Concrete.small_sections_of_hasLimit, CategoryTheory.OrthogonalReflection.instSmallLMultispanShape, small_zero, Nimber.small_Ico, 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, NatOrdinal.small_Ioc, small_map, Ordinal.small_Ioo, NatOrdinal.small_Iio, 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, NatOrdinal.small_Ico, NatOrdinal.small_Ioo, Submodule.FG.small, CategoryTheory.instSmallHomFunctorOppositeTypeColimitCompYoneda, small_quotient, CategoryTheory.Functor.instSmallColimitType, Countable.toSmall, small_plift, NatOrdinal.small_Icc, CategoryTheory.StructuredArrow.instSmallOfLocallySmall, Nimber.small_Iio, small_univ_iff, LightCondensed.instSmallHom, CategoryTheory.Localization.HasSmallLocalizedHom.small, small_iInter, small_add, NatOrdinal.small_Iic, ZFSet.small_coe, Ordinal.small_Ico, FirstOrder.Language.ElementarySubstructure.toModel.instSmall, 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