Structures · Algebra
Module.Finite
A module over a semiring is Module.Finite if it is finitely generated as a module.
- Defined in
- Mathlib.RingTheory.Finiteness.Defs
- Shape
- 2 explicit arguments · adds fg_top
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances13
- Int
- Nat
- ZMod
- Polynomial
- IsDedekindDomain.HeightOneSpectrum.adicCompletion
- FractionRing
- WithVal
- IsLocalRing.ResidueField
- Localization
- Localization.AtPrime
- Ideal.ResidueField
- Subtype
- HasQuotient.Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by984
- LinearMap.charpoly
- Module.finrank_pos
- Module.finrank_eq_rank
- Module.Finite.of_surjective
- Module.Finite.fg_top
- LinearMap.polyCharpoly
- Ideal.relNorm
- Module.rank_lt_aleph0
- Module.finBasis
- Module.finrank_eq_card_chooseBasisIndex
- NumberField.HeightOneSpectrum.adicAbv
- Module.Finite.equiv
- Submodule.finrank_le
- Ideal.spanNorm
- FractionalIdeal.absNorm
- Ideal.absNorm_span_singleton
- NumberField.HeightOneSpectrum.absNorm_ne_zero
- Module.Finite.trans
- IsIntegral.of_finite
- Submodule.finrank_quotient_add_finrank
- Module.Finite.of_restrictScalars_finite
- Submodule.finrank_mono
- LinearMap.nilRank
- Module.Finite.of_isLocalization
- Module.Finite.exists_fin'
- Module.support_eq_zeroLocus
- LieAlgebra.rank
- LinearMap.charpoly_toMatrix
- IsArtinianRing.of_finite
- Algebra.intTrace
- dualTensorHomEquiv
- Submodule.finrank_eq_zero
- Module.finrank_pos_iff
- IsAlgebraic.of_finite
- Module.Finite.finite_basis
- Ideal.inertiaDeg_pos
- NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal
- LieModule.rank
- FDRep.of
- Module.finite_of_finite
- Algebra.norm_localization
- LieAlgebra.IsRegular
- Module.free_of_flat_of_isLocalRing
- dualTensorHom_bijective
- Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator
- minpoly.natDegree_le
- SpecialLinearGroup.centerEquivRootsOfUnity
- NumberField.FinitePlace.norm_embedding
- AdicCompletion.ofTensorProductEquivOfFiniteNoetherian
- Module.finBasisOfFinrankEq
Ancestors0
No ancestors.