Theorems · Definition · commutative algebra

Ideal.primesOver.mk

{A : Type u_2} →
  [inst : CommSemiring A] →
    (p : Ideal A) →
      {B : Type u_3} →
        [inst_1 : Semiring B] →
          [inst_2 : Algebra A B] → (P : Ideal B) → [hPp : P.IsPrime] → [hp : P.LiesOver p] → ↑(p.primesOver B)

If an ideal P of B is prime and lying over p, then it is in primesOver p B.

Defined in

Mathlib.RingTheory.Ideal.Over

Cited by

3 results in Mathlib

Foundations

Depth 17 from the axioms · uses no axioms

Assumes

CommSemiringSemiringAlgebraIdeal.IsPrimeIdeal.LiesOver