Theorem isAssociatedPrime_iff

Modification history

2026-02-24 15:42
Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean
refactor(RingTheory/Ideal/AssociatedPrime/Basic): redefine associated primes to include a radical (#34221) …
Added isAssociatedPrime_iffView on Github →