Commit 2025-04-14 06:10 71d3df64

View on Github →

chore(LinearIndependent): rename linearCombination lemmas (#23045) Follow the naming convention around unnamespacing and appending _injective better. From Toric

Estimated changes

Modified Mathlib/LinearAlgebra/LinearIndependent/Basic.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Defs.lean

deleted theorem Fintype.linearIndependent_iff_injective

added theorem linearIndependent_iff_injective_finsuppLinearCombination

added theorem linearIndependent_iff_injective_fintypeLinearCombination

deleted theorem linearIndependent_iff_injective_linearCombination

Modified Mathlib/LinearAlgebra/RootSystem/Finite/g2.lean

Modified Mathlib/RingTheory/AlgebraicIndependent/Basic.lean