Theorem Ideal.mem_minimalPrimes_of_height_le

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) …

Added Ideal.mem_minimalPrimes_of_height_le View on Github →