Theorem finite_of_linearIndependent

Modification history

2023-12-30 03:42
Mathlib/RingTheory/Noetherian.lean
chore: deduplicate `LinearIndependent.set_finite_of_isNoetherian` (#9300) …
Deleted finite_of_linearIndependentView on Github →
2023-10-10 23:14
Mathlib/RingTheory/Noetherian.lean
feat: improve API for Fitting decomposition of a linear endomorphism (#7487) …
Modified finite_of_linearIndependentView on Github →
2023-03-20 19:32
Mathlib/RingTheory/Noetherian.lean
feat: port RingTheory.Noetherian (#2976)
Added finite_of_linearIndependentView on Github →