Commit 2023-08-03 08:06 73993336

View on Github →

chore(LinearAlgebra): remove open Classical (#6320) This uncovers a few situations where a lemma was stated with the wrong decidability assumption. The corrected lemmas are strictly more syntactically-general. This is exhaustive in the LinearAlgebra folder. Where removal is impractical, this switches to open Classical in to make the intent clear.

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean

modified theorem AffineIndependent.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one

modified theorem AffineIndependent.finrank_vectorSpan_image_finset

modified theorem AffineIndependent.vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one

modified theorem finrank_vectorSpan_image_finset_le

Modified Mathlib/LinearAlgebra/Charpoly/Basic.lean

Modified Mathlib/LinearAlgebra/Charpoly/ToMatrix.lean

modified theorem LinearMap.charpoly_toMatrix

Modified Mathlib/LinearAlgebra/Contraction.lean

Modified Mathlib/LinearAlgebra/Determinant.lean

Modified Mathlib/LinearAlgebra/Dimension.lean

Modified Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

Modified Mathlib/LinearAlgebra/Dual.lean

modified theorem Subspace.dual_finrank_eq

Modified Mathlib/LinearAlgebra/FiniteDimensional.lean

Modified Mathlib/LinearAlgebra/Finrank.lean

Modified Mathlib/LinearAlgebra/Finsupp.lean

modified def Finsupp.supported

modified theorem Fintype.total_apply_single

Modified Mathlib/LinearAlgebra/FinsuppVectorSpace.lean

Modified Mathlib/LinearAlgebra/FreeModule/Basic.lean

Modified Mathlib/LinearAlgebra/InvariantBasisNumber.lean

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

modified theorem Fintype.linearIndependent_iff'

Modified Mathlib/LinearAlgebra/Span.lean

Modified Mathlib/LinearAlgebra/Trace.lean