Inductive IsFiniteLength

Modification history

2025-02-12 07:31

Mathlib/RingTheory/FiniteLength.lean

feat(RingTheory): Hopkins–Levitzki theorem (#21451) …

Modified IsFiniteLength View on Github →

2024-10-09 07:18

Mathlib/RingTheory/FiniteLength.lean

feat: define finite length modules and show equivalence with `IsNoetherian ∧ IsArtinian` (#17478) …

Added IsFiniteLength View on Github →