Theorem Ideal.Filtration.mem_submodule

Modification history

2026-07-04 08:56

Mathlib/RingTheory/Filtration.lean

refactor(Algebra): make `MonoidAlgebra` into a one-field structure (#38714) …

Modified Ideal.Filtration.mem_submodule View on Github →

2023-06-01 12:52

Mathlib/RingTheory/Filtration.lean

feat: port RingTheory.Filtration (#4488)

Added Ideal.Filtration.mem_submodule View on Github →