Theorem Module.Finite.finite_basis

Modification history

2024-11-14 10:43
Mathlib/RingTheory/Finiteness.lean
chore(RingTheory): split Finiteness.lean into many smaller files (#18964) …
Modified Module.Finite.finite_basisView on Github →
2024-10-23 01:35
Mathlib/RingTheory/Finiteness.lean
chore: generalize from `AddCommGroup` to `AddCommMonoid` (#18095) …
Modified Module.Finite.finite_basisView on Github →
2024-09-10 08:39
Mathlib/RingTheory/Finiteness.lean
feat: generalize Module.Finite.finite_basis to semirings (#16655)
Modified Module.Finite.finite_basisView on Github →
2024-01-01 14:48
Mathlib/RingTheory/Finiteness.lean
chore: Reorganize results about `rank` and `finrank`. (#9349) …
Added Module.Finite.finite_basisView on Github →