Structures · Algebra
IsNoetherian
IsNoetherian R M is the proposition that M is a Noetherian R-module,
implemented as the predicate that all R-submodules of M are finitely generated.
- Defined in
- Mathlib.RingTheory.Noetherian.Defs
- Shape
- 2 explicit arguments · adds noetherian
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by4
Concrete types that are instances5
- Int
- Nat
- Polynomial
- NumberField.RingOfIntegers
- HasQuotient.Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by191
- IsNoetherian.noetherian
- LieModule.chainTopCoeff
- LieAlgebra.corootSpace
- LieModule.chainBotCoeff
- LieModule.chainTop
- Module.Finite.of_injective
- LieModule.coe_chainTop
- LieAlgebra.rootSpace_zero_eq
- IsNoetherian.finsetBasisIndex
- LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add
- LieAlgebra.Basis.isCartanSubalgebra
- LieModule.chainBot
- IsNoetherian.finsetBasis
- LieModule.chainTopCoeff_zero
- Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndex
- isNoetherian_of_surjective
- LieModule.genWeightSpace_add_chainTop
- LieAlgebra.mem_corootSpace
- isNoetherian_of_linearEquiv
- LieModule.eventually_genWeightSpace_smul_add_eq_bot
- LieModule.chainBotCoeff_zero
- Module.End.maxGenEigenspace_eq
- LieModule.genWeightSpace_nsmul_add_ne_bot_of_le
- IsNoetherian.injective_of_surjective_of_injective
- LieModule.coe_chainTop'
- LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra
- LieModule.chainBotCoeff_neg
- LieModule.isNilpotent_iff_forall'
- LinearIndependent.set_finite_of_isNoetherian
- IsSl2Triple.HasPrimitiveVectorWith.exists_nat
- LinearMap.eventually_iSup_ker_pow_eq
- LieModule.isNilpotent_iff_forall
- LieModule.exists_genWeightSpace_smul_add_eq_bot
- LieIdeal.isSolvable_of_killingForm_apply_lie_eq_zero
- LieAlgebra.mem_corootSpace'
- RingTheory.Sequence.IsWeaklyRegular.of_perm_of_subset_jacobson_annihilator
- LieModule.isNilpotent_toEnd_sub_algebraMap
- isNoetherian_of_le
- LieAlgebra.zeroRootSubalgebra_eq_of_is_cartan
- LieAlgebra.isNilpotent_iff_forall
- IsNoetherian.induction
- LieAlgebra.LieIdeal.solvable_iff_le_radical
- fg_of_injective
- LinearMap.charpoly_nilpotent_tfae
- LinearMap.isCompl_iSup_ker_pow_iInf_range_pow
- LieModule.exists_forall_lie_eq_smul
- LieModule.chainTopCoeff_neg
- FiniteDimensional.left
- LieModule.chainTopCoeff_add_one
- Subalgebra.fg_of_noetherian
Ancestors0
No ancestors.