Theorem isAssociatedPrime_iff_exists_injective_linearMap

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) …
Modified isAssociatedPrime_iff_exists_injective_linearMapView on Github →
2025-05-01 08:12
Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean
feat(RingTheory/Ideal/AssociatedPrime/Basic): associated primes and exact sequence (#24453) …
Added isAssociatedPrime_iff_exists_injective_linearMapView on Github →