Structures · Algebra
IsPrincipalIdealRing
A ring is a principal ideal ring if all (left) ideals are principal.
- Defined in
- Mathlib.RingTheory.Ideal.Span
- Shape
- One type argument · adds principal
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances4
- Localization
- DualNumber
- Subtype
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by138
- Ideal.span_singleton_dvd_span_singleton_iff_dvd
- Submodule.smithNormalFormCoeffs
- Ideal.smithCoeffs
- Ideal.normalizedFactorsEquivSpanNormalizedFactors
- Algebra.denominator
- IsPrincipalIdealRing.of_surjective
- Submodule.smithNormalFormBotBasis
- PrincipalIdealRing.isMaximal_of_irreducible
- Ideal.selfBasis
- PrincipalIdealRing.factors
- Submodule.smithNormalFormTopBasis
- Ideal.ringBasis
- Submodule.smithNormalForm
- Algebra.denominator_dvd_iff
- Ideal.emultiplicity_eq_emultiplicity_span
- LieModule.trace_toEnd_genWeightSpace
- isCoprime_of_irreducible_dvd
- Ideal.finrank_eq_finrank
- Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity
- Module.equiv_free_prod_directSum
- Ideal.count_span_normalizedFactors_eq
- Ideal.torsionOf_eq_span_pow_pOrder
- Submodule.basisOfPid
- LieModule.weightSpaceOfIsLieTower
- OnePoint.exists_mem_SL2
- LieSubmodule.trace_eq_trace_restrict_of_le_idealizer
- Submodule.basis_of_pid_aux
- Submodule.smithNormalFormBotBasis_def
- Submodule.exists_smith_normal_form_of_rank_eq
- PrincipalIdealRing.factors_spec
- Module.equiv_directSum_of_isTorsion
- Ideal.count_span_normalizedFactors_eq_of_normUnit
- Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity
- IsPrincipalIdealRing.ringKrullDim_eq_one
- IsIntegralClosure.module_free
- LieIdeal.killingForm_eq
- Ideal.isPrime_iff_of_isPrincipalIdealRing_of_noZeroDivisors
- Module.basisOfFiniteTypeTorsionFree
- Module.torsion_by_prime_power_decomposition
- LieSubmodule.traceForm_eq_of_le_idealizer
- LieIdeal.le_killingCompl_top_of_isLieAbelian
- IsIntegralClosure.rank
- LieModule.traceForm_genWeightSpace_eq
- Ideal.quotientEquivDirectSum
- Module.exists_smul_eq_zero_and_mk_eq
- Submodule.quotientEquivDirectSum
- LinearMap.trace_restrict_eq_of_forall_mem
- isCoprime_of_prime_dvd
- card_classGroup_eq_one
- Ideal.finrank_quotient_eq_sum
Ancestors0
No ancestors.