Theorem Module.freeLocus_eq_univ

Modification history

2025-10-31 11:48

Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean

feat(Algebra): congruence relation respecting SMul (#30665)

Modified Module.freeLocus_eq_univ View on Github →

2024-11-25 08:40

Mathlib/Algebra/Module/FreeLocus.lean

feat: the free locus of a (finitely presented) module (#18691)

Added Module.freeLocus_eq_univ View on Github →