Module

Ideal_eq_of_le_of_mem_of_mem_minimalPrimes_iff_notMem.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_eq_of_le_of_mem_of_mem_minimalPrimes_iff_notMem

1 declaration indexed from sourceView source ↗

Module documentation

Ideal eq of le of mem of mem minimal Primes iff not Mem

Imports1

Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Imported by2

theorem

eq_of_le_of_mem_of_mem_minimalPrimes_iff_notMem

L24 ↗

Ideal.eq_of_le_of_mem_of_mem_minimalPrimes_iff_notMem

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_eq_of_le_of_mem_of_mem_minimalPrimes_iff_notMem

Lean source · statement

theorem _root_.Ideal.eq_of_le_of_mem_of_mem_minimalPrimes_iff_notMem
    {B : Type*} [CommRing B] [IsNoetherianRing B] {π : B} {Q Q' : Ideal B}
    [Q.IsPrime] [Q'.IsPrime] (hle : Q' ≤ Q) (hπ : π ∈ Q')
    (h : ∀ p : Ideal B, p.IsPrime → p ≤ Q → (p ∈ minimalPrimes B ↔ π ∉ p)) : Q' = Q

Module documentation

Ideal eq of le of mem of mem minimal Primes iff not Mem

Declarations

eq_of_le_of_mem_of_mem_minimalPrimes_iff_notMem