Theorem Module.Finite.exists_fin'

Modification history

2025-08-11 10:26

Mathlib/RingTheory/Finiteness/Cardinality.lean

feat(RingTheory/Finiteness): add `Submodule.fg_iff_exists_fin_linearMap` (#27957) …

Modified Module.Finite.exists_fin'View on Github →

2024-11-14 10:43

Mathlib/RingTheory/Finiteness.lean

chore(RingTheory): split Finiteness.lean into many smaller files (#18964) …

Modified Module.Finite.exists_fin'View on Github →

2024-10-03 19:18

Mathlib/RingTheory/Finiteness.lean

chore: Rename `FiniteDimensional.finrank` to `Module.finrank` (#17192) …

Modified Module.Finite.exists_fin'View on Github →

2024-04-29 23:31

Mathlib/RingTheory/Finiteness.lean

feat(RingTheory/Finiteness): relax the condition of `Module.Finite.exists_fin'` (#12524) …

Modified Module.Finite.exists_fin'View on Github →

2023-09-21 09:45

Mathlib/RingTheory/Finiteness.lean

feat: `Hom(N, M)` is Noetherian when `M` is Noetherian and `N` is finitely-generated. (#7276)

Added Module.Finite.exists_fin'View on Github →