Structures · Algebra
Ideal.IsMaximal
An ideal is maximal if it is maximal in the collection of proper ideals.
- Defined in
- Mathlib.RingTheory.Ideal.Maximal
- Shape
- One type argument · adds out
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- Int
- Polynomial
- MvPolynomial
How is a type an instance?
Loading the hierarchy index…
Assumed by159
- Ideal.Quotient.field
- Ideal.IsMaximal.out
- Ideal.comap_isMaximal_of_surjective
- IsLocalization.AtPrime.equivQuotMaximalIdeal
- Ideal.exists_ideal_over_maximal_of_isIntegral
- IsLocalization.AtPrime.equivQuotientMapOfIsMaximal
- IsDedekindDomain.primesOver_ncard_ne_zero
- Ideal.IsMaximal.of_liesOver_isMaximal
- Ideal.inertiaDeg_eq_of_isMaximal
- IsDedekindDomain.coe_primesOverFinset
- Ideal.sum_ramification_inertia
- IsDedekindDomain.mem_primesOverFinset_iff
- AdicCompletion.isMaximal_map_of_le
- Ideal.isCoprime_of_isMaximal
- Ideal.IsMaximal.mul_mem_pow
- Ideal.exists_maximal_ideal_liesOver_of_isIntegral
- Algebra.trace_quotient_eq_of_isDedekindDomain
- Ideal.eq_prime_pow_mul_coprime
- Ideal.isMaximal_comap_of_isIntegral_of_isMaximal'
- Ideal.inertiaDeg'_ne_zero
- Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
- IsDedekindDomain.HeightOneSpectrum.equivPrimesOver
- Ideal.bot_lt_of_maximal
- Ideal.comap_map_eq_self_of_isMaximal
- Ideal.toCharacterSpace
- Ideal.IsMaximal.ne_bot_of_isIntegral_int
- Ideal.inertiaDeg'_eq_inertiaDeg
- Ideal.IsMaximal.of_isLocalization_of_disjoint
- Ideal.mem_primesOver_iff_mem_normalizedFactors
- IsLocalization.AtPrime.equivQuotientMapMaximalIdeal
- IsLocalization.AtPrime.equivQuotMaximalIdealPow
- pow_sub_one_dvd_differentIdeal
- Ideal.map_algebraMap_eq_finsetProd_pow
- IsDedekindDomain.primesOver_finite
- Ideal.cardQuot_pow_inertiaDeg
- Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing
- PrimeSpectrum.exists_multiset_prod_cons_le_and_prod_not_le
- not_dvd_differentIdeal_of_isCoprime_of_isSeparable
- Ideal.isOpen_pow_of_isMaximal
- Ideal.relNorm_eq_pow_of_isMaximal
- IsLocalization.AtPrime.under_maximalIdeal_pow
- Ideal.finrank_quotient_map
- Ideal.toCharacterSpace_apply_eq_zero_of_mem
- Polynomial.height_map_C
- IsInertiaField.rank_right
- IsLocalization.AtPrime.algebraMap_equivQuotMaximalIdeal_symm_apply
- trace_quotient_eq_trace_localization_quotient
- IsCyclotomicExtension.Rat.mem_zpowers_galEquivZMod_of_mem_stabilizer
- Ideal.finrank_prime_pow_ramificationIdx
- IsLocalization.AtPrime.under_map_eq_map
Ancestors0
No ancestors.