Theorem Module.stableUnderSpecialization_support

Modification history

2025-11-07 17:06

Mathlib/RingTheory/Spectrum/Prime/Module.lean

chore(RingTheory/Spectrum/Prime/Module): golf `stableUnderSpecialization_support` using `mem_support_mono` (#30148) …

Modified Module.stableUnderSpecialization_support View on Github →

2024-07-22 15:39

Mathlib/AlgebraicGeometry/PrimeSpectrum/Module.lean

feat(RingTheory/Support): Define support of a module (#14507) …

Added Module.stableUnderSpecialization_support View on Github →