Commit 2024-12-02 15:15 0429dca7

View on Github →

chore: defer a lemma, to avoid needing Cardinal in LinearIndependent (#19626)

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

Modified Mathlib/Analysis/Convex/Cone/Basic.lean

Modified Mathlib/Analysis/LocallyConvex/Polar.lean

Modified Mathlib/LinearAlgebra/Dimension/Basic.lean

Modified Mathlib/LinearAlgebra/Dimension/Finite.lean

added theorem linearIndependent_bounded_of_finset_linearIndependent_bounded

Modified Mathlib/LinearAlgebra/Finsupp/VectorSpace.lean

Modified Mathlib/LinearAlgebra/FreeModule/Basic.lean

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

deleted theorem linearIndependent_bounded_of_finset_linearIndependent_bounded

Modified Mathlib/RingTheory/TensorProduct/Free.lean