Finite

📁 Source: Mathlib/Algebra/Module/Presentation/Finite.lean

Statistics

Metric	Count
Definitions Finite	1
Theorems finite, finitePresentation, finitePresentation_iff_exists_presentation	3
Total	4

Module

Definitions

Name	Category	Theorems
Finite 📖	CompData	191 math math: Finite.instLocalizationLocalizedModule, FreeAbelianGroup.instFiniteInt, rank_lt_aleph0_iff, Finite.of_surjective, IsCyclotomicExtension.finite, Algebra.finite_adjoin_simple_of_isIntegral, WithLp.instModuleFinite, finite_of_finite_type_of_isJacobsonRing, Algebra.instFiniteResidueFieldOfQuasiFiniteAt, Presentation.finite, Algebra.WeaklyQuasiFiniteAt.finite_residueField, Algebra.QuasiFinite.iff_of_isArtinianRing, QuadraticAlgebra.instFinite, TensorProduct.exists_finite_submodule_of_finite', FGModuleCat.instFiniteHomModuleCatObjIsFG, ZLattice.module_finite, Representation.instFiniteAsModule, finite_of_finrank_pos, Finite.left, finite_iff_isArtinianRing, Finite.of_finite, FinitePresentation.equiv_quotient, ModuleCat.isFG_iff, RootPairing.instFiniteSubtypeMemSubmoduleRootSpanOfFinite, AddMonoidAlgebra.moduleFinite, dual_finite, TensorProduct.exists_finite_submodule_left_of_setFinite, finite_of_algHom_finiteType_of_isJacobsonRing, Algebra.instFiniteResidueFieldOfFormallyUnramified, finite_of_isSemisimpleRing, NumberField.Units.instFiniteIntAdditiveUnitsRingOfIntegers, AEval.instFiniteOrig, IsAdjoinRootMonic.finite, Algebra.IsIntegral.finite, IsCyclotomicExtension.finite_of_singleton, IntermediateField.instFiniteSubtypeMemBot, Algebra.Extension.Cotangent.finite, FGModuleCat.instFiniteHom, instFiniteCarrier, finite_of_rank_eq_nat, Algebra.WeaklyQuasiFiniteAt.finite_locoalization, Algebra.instFiniteOfIsQuadraticExtension, Finite.prod, instModuleFinite, TensorProduct.exists_finite_submodule_right_of_setFinite, Finite.right, Finite.quotient, Invertible.instFinite, RootPairing.instFiniteSubtypeMemSubmoduleCorootSpanOfFinite, finite_of_isArtinianRing, Polynomial.degreeLT.instFiniteSubtypeMemSubmodule, not_finite_of_infinite_basis, Finite.ulift, FGModuleCat.instFiniteCarrierLimitModuleCatCompForget₂LinearMapIdObjIsFG, Finite.linearMap, TensorProduct.exists_finite_submodule_left_of_finite, instFiniteSubtypeMemIdealOfIsNoetherian, Finite.of_injective, Algebra.QuasiFinite.finite_fiber, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux₂, Algebra.QuasiFinite.instFiniteResidueField, finite_iff_finite, Algebra.instFiniteH1CotangentOfFinitePresentationOfProjectiveKaehlerDifferential, FiniteField.instFiniteExtension_1, IsIntegralClosure.finite, KaehlerDifferential.finite, Localization.finite_of_primesOver_eq_singleton, TensorProduct.exists_finite_submodule_right_of_setFinite', MonoidAlgebra.moduleFinite, IsSemisimpleModule.finite_tfae, Algebra.instFiniteResidueFieldOfIsUnramifiedAt, Finite.of_isLocalization, Polynomial.Monic.finite_adjoinRoot, module_finite_of_liesOver, AddMonoid.FG.to_moduleFinite_nat, Grassmannian.finite_quotient, instFiniteOfFinitePresentation, Finite.of_isComplemented_domain, Finite.of_isLocalizedModule, instModuleFinite_of_discrete_submodule, TensorProduct.exists_finite_submodule_left_of_finite', Finite.addMonoidHom, TensorProduct.exists_finite_submodule_of_finite, Finite.of_submodule_quotient, MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictDegreeOfFinite, Ring.instFiniteNormalClosure, Finite.of_restrictScalars_finite, IsSemiprimaryRing.isNoetherian_iff_finite_of_jacobson_fg, FGModuleCat.instFiniteCarrierColimitModuleCatCompForget₂LinearMapIdObjIsFG, RingHom.finite_algebraMap, Finite.instMulOpposite, Finite.span_singleton, Algebra.finite_adjoin_of_finite_of_isIntegral, QuaternionAlgebra.instFinite, Finite.of_finite_tensorProduct_of_faithfullyFlat, Polynomial.Monic.finite_quotient, Finite.range, IsNoetherian.iff_fg, finite_of_finrank_eq_succ, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, Subalgebra.finite_sup, Finite.self, finite_iff_of_rank_eq_nsmul, LinearMap.finite_of_det_ne_one, finite_def, MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictTotalDegreeOfFinite, TensorProduct.exists_finite_submodule_of_setFinite', finite_finsupp_iff, exteriorPower.instFinite, instFiniteAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, FiniteDimensional.right, FGModuleRepr.instFiniteRepr, IsArtinianRing.tfae, instFiniteFractionRingLocalizationAlgebraMapSubmonoidNonZeroDivisors, finite_of_rank_eq_one, Finite.trans, Finite.of_exact, Finite.of_equiv_equiv, finite_dual_iff, Finite.equiv_iff, IsLocalRing.ResidueField.finite_of_module_finite, instFiniteResidueField, PowerBasis.finite, Finite.top, finite_of_rank_eq_zero, Finite.of_pi, instFiniteLocalizationAlgebraMapSubmonoidPrimeCompl, MvPolynomial.instFiniteOfIsEmpty, ModuleCat.finite_ext, instFiniteCarrierObjModuleCatIsFG, Ring.instFiniteNormalClosure_1, Finite.iff_fg, Finite.of_fg, finite_iff_krullDimLE_zero, TensorProduct.exists_finite_submodule_right_of_finite, Finite.map, Submodule.finite_dualAnnihilator_iff, TensorProduct.exists_finite_submodule_right_of_finite', FGModuleCat.instFiniteCarrier, FDRep.instFiniteCarrierVFGModuleCat, Finite.of_basis, FiniteDimensional.left, Finite.bot, TensorProduct.exists_finite_submodule_of_setFinite, TensorProduct.exists_finite_submodule_left_of_setFinite', AEval.instFinitePolynomial, Finite.iff_addMonoid_fg, Finite.span_finset, Finite.instLinearMapIdSubtypeMemSubmoduleOfIsSemisimpleModule_1, finite_finsupp_self_iff, Ideal.Quotient.finite_of_isInvariant, Submodule.IsLattice.finite, Finite.matrix, IsAzumaya.toFinite, Finite.span_of_finite, LinearMap.finite_iff_of_bijective, NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, Polynomial.instFiniteUniversalFactorizationRing, NumberField.Units.instFiniteIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion, finitePresentation_iff_finite, IsLocalRing.instFiniteResidueField, Finite.base_change, Finite.iff_addGroup_fg, Finite.equiv, Submodule.finite_sup, ModN.instModuleFinite, IsNoetherian.finite, Finite.of_quasiFinite, IsSemiprimaryRing.finite_of_isArtinian, AddMonoid.FG.to_moduleFinite_int, Finite.finsupp, Algebra.Etale.iff_exists_algEquiv_prod, Algebra.finite_iff_isIntegral_and_finiteType, Finite.tensorProduct, Algebra.FormallyUnramified.finite_of_free, Quaternion.instFinite, Finite.pi_iff, Finite.iff_cofg_bot, Finite.Module.finite_shrink, IsSemiprimaryRing.finite_of_isNoetherian, SeparationQuotient.instModuleFinite, ContinuousLinearMap.instModuleFinite, Algebra.finite_of_essFiniteType_of_isAlgebraic, WithCStarModule.instModuleFinite, Polynomial.not_finite, instFinitePolynomialAEval', finite_of_surjective_of_ker_le_nilradical, Finite.of_isComplemented_codomain, Finite.instLinearMapIdSubtypeMemSubmoduleOfIsSemisimpleModule, IntermediateField.finite_of_fg_of_isAlgebraic, Subalgebra.finite_bot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finitePresentation_iff_exists_presentation 📖	mathematical	—	FinitePresentation Ring.toSemiring AddCommGroup.toAddCommMonoid Finite Relations.G Presentation.toRelations Relations.R	—	Submodule.fg_iff_exists_finite_generating_family finite_def instFiniteOfFinitePresentation FinitePresentation.fg_ker Finite.finsupp Finite.self RingHomSurjective.ids LinearMap.range_eq_top Finsupp.range_linearCombination Submodule.ext_iff Submodule.subset_span Relations.Solution.isPresentation_iff Presentation.finitePresentation

Module.Presentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite 📖	mathematical	—	Module.Finite Ring.toSemiring AddCommGroup.toAddCommMonoid	—	Module.Finite.of_surjective RingHomSurjective.ids Module.Finite.finsupp Module.Finite.self Module.Relations.Solution.IsPresentation.surjective_π toIsPresentation
finitePresentation 📖	mathematical	—	Module.FinitePresentation Ring.toSemiring AddCommGroup.toAddCommMonoid	—	Module.finitePresentation_of_surjective instFinitePresentationFinsupp Module.Relations.Solution.IsPresentation.surjective_π toIsPresentation Module.Relations.Solution.IsPresentation.ker_π Submodule.fg_span Set.finite_range

---

← Back to Index