Structure Ideal.Filtration

Modification history

2024-12-03 16:13

Mathlib/RingTheory/Filtration.lean

chore: Generalize universes in `RingTheory/Filtration` (#19677)

Modified Ideal.Filtration View on Github →

2023-06-01 12:52

Mathlib/RingTheory/Filtration.lean

feat: port RingTheory.Filtration (#4488)

Added Ideal.Filtration View on Github →