Commit 2025-05-10 21:30 ced17eed

View on Github →

feat: LinearIndepOn versions of existing LinearIndependent lemmas (#24747) From Toric

Estimated changes

Modified Mathlib/LinearAlgebra/LinearIndependent/Basic.lean

deleted theorem LinearIndepOn.mono

Modified Mathlib/LinearAlgebra/LinearIndependent/Defs.lean

added theorem LinearIndepOn.mono

added theorem linearIndepOn_finset_iff

added theorem linearIndepOn_finset_iffₛ

added theorem linearIndepOn_iff_linearIndepOn_finset

added theorem not_linearIndepOn_finset_iff

added theorem not_linearIndepOn_finset_iffₛ

Modified Mathlib/RingTheory/Flat/Basic.lean

modified theorem LinearIndependent.tmul_of_flat_left

modified theorem LinearIndependent.tmul_of_flat_right

Modified Mathlib/RingTheory/Flat/Domain.lean

modified theorem LinearIndependent.tmul_of_isDomain

modified theorem TensorProduct.map_injective_of_flat_flat_of_isDomain