Theorem Ideal.IsMinimalPrime.isPrime

Modification history

2026-05-13 10:08
Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean
refactor(RingTheory): refactor APIs for minimal primes to lessen defeq abuse (#38029) …
Added Ideal.IsMinimalPrime.isPrimeView on Github →