Theorem Ideal.mem_minimalPrimes_of_height_eq

Modification history

2026-07-28 08:55

Mathlib/RingTheory/Ideal/Height.lean

fix(RingTheory/Ideal/Height): mem_minimalPrimes_of_height_eq should be mem_minimalPrimes_of_height_le (#42088) …

Deleted Ideal.mem_minimalPrimes_of_height_eq View on Github →

2025-03-13 07:17

Mathlib/RingTheory/Ideal/Height.lean

feat(RingTheory/Ideal): more lemmas about the height of an ideal (#21041) …

Added Ideal.mem_minimalPrimes_of_height_eq View on Github →