Commit 2025-01-15 15:07 e9a89abf

View on Github →

chore: generalize more materials about linear independence over semirings (#20497) Also add Finsupp.linearCombination_one_tmul and linearIndependent_one_tmul that connects linear independence to flatness.

Estimated changes

Modified Mathlib/LinearAlgebra/Basis/Basic.lean

Modified Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

added theorem Finsupp.linearCombination_one_tmul

Modified Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean

added theorem Finsupp.linearCombination_smul

Modified Mathlib/RingTheory/Adjoin/PowerBasis.lean

Modified Mathlib/RingTheory/AdjoinRoot.lean

Modified Mathlib/RingTheory/AlgebraTower.lean

modified theorem linearIndependent_smul

Modified Mathlib/RingTheory/Flat/Basic.lean

added theorem Module.Flat.linearIndependent_one_tmul

Modified Mathlib/RingTheory/Localization/Module.lean

modified theorem LinearIndependent.localization

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

modified theorem Algebra.baseChange_lmul