Commit 2025-05-09 11:18 1296581e

View on Github →

chore(LinearAlgebra): golfs around linearIndependent_single (#24209) also generalize to semirings

Estimated changes

Modified Mathlib/LinearAlgebra/Finsupp/VectorSpace.lean

added theorem DFinsupp.linearIndependent_single

added theorem DFinsupp.linearIndependent_single_iff

modified theorem Finsupp.linearIndependent_single

modified theorem Finsupp.linearIndependent_single_iff

Modified Mathlib/LinearAlgebra/StdBasis.lean

modified theorem Pi.linearIndependent_single

modified theorem Pi.linearIndependent_single_one