Commit 2023-08-03 10:45 92f695f0

View on Github →

refactor(LinearAlgebra): Ensure ChooseBasisIndex is finite on trivial modules (#6322) This also changes basisFintypeOfFiniteSpans to use Finite rather than Fintype, as it was noncomputable anyway. This means it has to be renamed to basis_finite_of_finite_spans as it now is a proof!

Estimated changes

Modified Mathlib/FieldTheory/Tower.lean

modified theorem FiniteDimensional.finrank_mul_finrank'

Modified Mathlib/LinearAlgebra/Contraction.lean

Modified Mathlib/LinearAlgebra/Dimension.lean

deleted def basisFintypeOfFiniteSpans

added theorem basis_finite_of_finite_spans

Modified Mathlib/LinearAlgebra/Dual.lean

modified theorem Module.dual_rank_eq

modified theorem Module.erange_coe

Modified Mathlib/LinearAlgebra/FreeModule/Basic.lean

modified def Module.Free.ChooseBasisIndex

Modified Mathlib/LinearAlgebra/FreeModule/Finite/Basic.lean

Modified Mathlib/LinearAlgebra/FreeModule/Finite/Rank.lean

Modified Mathlib/LinearAlgebra/Trace.lean