Commit 2026-07-28 08:55 cc3705d1
View on Github →fix(RingTheory/Ideal/Height): mem_minimalPrimes_of_height_eq should be mem_minimalPrimes_of_height_le (#42088)
According to the theorem statement and docstring, Ideal.mem_minimalPrimes_of_height_eq introduced in #21041 should be named Ideal.mem_minimalPrimes_of_height_le. This PR renames it accordingly.