Commit 2023-12-30 03:42 7392ea7c

View on Github →

chore: deduplicate LinearIndependent.set_finite_of_isNoetherian (#9300) Also moved several lemmas into Mathlib/LinearAlgebra/Basis.lean.

Estimated changes

Modified Mathlib/FieldTheory/Finiteness.lean

Modified Mathlib/LinearAlgebra/Basis.lean

added theorem basis_finite_of_finite_spans

added theorem infinite_basis_le_maximal_linearIndependent'

added theorem infinite_basis_le_maximal_linearIndependent

added theorem union_support_maximal_linearIndependent_eq_range_basis

Modified Mathlib/LinearAlgebra/Dimension.lean

deleted theorem LinearIndependent.finite_of_isNoetherian

deleted theorem LinearIndependent.set_finite_of_isNoetherian

deleted theorem basis_finite_of_finite_spans

deleted theorem infinite_basis_le_maximal_linearIndependent'

deleted theorem infinite_basis_le_maximal_linearIndependent

deleted theorem union_support_maximal_linearIndependent_eq_range_basis

Modified Mathlib/LinearAlgebra/FiniteDimensional.lean

Modified Mathlib/RingTheory/Noetherian.lean

added theorem LinearIndependent.finite_of_isNoetherian

added theorem LinearIndependent.set_finite_of_isNoetherian

deleted theorem finite_of_linearIndependent