Structures · Algebra
Ideal.LiesOver
P lies over p if p is the preimage of P by the algebraMap.
- Defined in
- Mathlib.RingTheory.Ideal.Over
- Shape
- 2 explicit arguments · adds over
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Int
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by266
- Ideal.over_def
- Localization.AtPrime.algebraOfLiesOver
- Ideal.LiesOver.over
- Ideal.LiesOver.trans
- Ideal.inertiaDegIn_eq_inertiaDeg
- Ideal.inertiaDeg'_algebraMap
- Ideal.ramificationIdxIn_eq_ramificationIdx
- Ideal.Quotient.stabilizerHom
- IsFractionRing.stabilizerHom
- Ideal.inertiaDeg_tower
- Ideal.inertiaDeg_eq
- Ideal.exists_smul_eq_of_isGaloisGroup
- Ideal.IsDedekindDomain.ramificationIdx'_ne_zero_of_liesOver
- Ideal.ramificationIdx_eq
- IsLocalization.AtPrime.isPrime_map_of_liesOver
- Polynomial.residueFieldMapCAlgEquiv
- Ideal.ramificationIdx_tower
- Ideal.eq_bot_of_liesOver_bot
- IsLocalization.AtPrime.equivQuotientMapOfIsMaximal
- Ideal.fiberIsoOfBijectiveResidueField
- Ideal.ne_bot_of_liesOver_of_ne_bot
- Ideal.natAbs_pow_inertiaDeg
- Ideal.IsMaximal.of_liesOver_isMaximal
- Ideal.inertiaDeg_eq_of_isMaximal
- Ideal.isPrime_of_liesOver
- Ideal.ramificationIdx'_eq_ramificationIdx'
- Ideal.disjoint_primeCompl_of_liesOver
- Ideal.inertiaDeg'_ne_zero
- Ideal.pow_inertiaDeg
- IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver
- Ideal.IsFractionRing.normal
- Ideal.inertiaDeg_below_dvd
- Ideal.Quotient.algEquivOfEqComap
- Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count
- Ideal.card_inertia_eq_ramificationIdxIn
- IsFractionRing.stabilizerQuotientInertiaEquiv
- Ideal.IsFractionRing.finite_of_isInvariant
- Ideal.card_stabilizer_eq
- Ideal.comap_fiberIsoOfBijectiveResidueField_symm
- Ideal.card_stabilizer_eq_card_inertia_mul_finrank
- Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count
- Ideal.ramificationIdx_below_dvd
- IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver'
- Ideal.exists_ideal_le_liesOver_of_le
- Ideal.inertiaDeg'_eq_inertiaDeg
- Ideal.IsDedekindDomain.ramificationIdx_eq_multiplicity
- Ideal.Quotient.ker_stabilizerHom
- Algebra.isUnramifiedAt_iff_map_eq
- IsFractionRing.stabilizerHom_surjective
- Ideal.inertiaDeg_eq_of_isGaloisGroup
Ancestors0
No ancestors.