Theorems · Theorem · commutative algebra
Ideal.LiesOver.over
∀ {A : Type u_2} {inst : CommSemiring A} {B : Type u_3} {inst_1 : Semiring B} {inst_2 : Algebra A B} {P : Ideal B}
{p : Ideal A} [self : P.LiesOver p], p = Ideal.under A P- Defined in
- Mathlib.RingTheory.Ideal.Over
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext
- Assumes
- Ideal.LiesOver
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- Idealstatement and proof · cited by 4,748
- Ideal.LiesOverstatement and proof · cited by 272
- Ideal.understatement · cited by 170
Cited by25
Results whose statement or proof uses this declaration.
- Ideal.over_defproof · cited by 60
- Ideal.inertiaDeg_defproof · cited by 4
- Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComapproof · cited by 4
- Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eqstatement · cited by 3
- Algebra.IsInvariant.orbit_eq_primesOverproof · cited by 2
- Algebra.isUnramifiedAt_iff_map_eqproof · cited by 2
- IsArithFrobAt.exists_primesOver_isConjproof · cited by 2
- Ideal.exists_ltSeries_of_hasGoingDownproof · cited by 1
- Ideal.map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimesproof · cited by 1
- dvd_differentIdeal_of_not_isSeparableproof · cited by 1
- IsUnramifiedAt.of_liesOver_of_ne_botproof · cited by 1
- Algebra.QuasiFinite.finite_primesOverproof · cited by 1