Commit 2025-02-20 19:11 53083245

refactor(LinearIndependent): refactor to use LinearIndepOn (#21886) Currently, if s is a set of vectors in a module W, the way to state that the vectors in s are linearly independent is LinearIndependent R (Subtype.val : ↥s → W) (or similar), and if v : ι -> W and s : Set ι is a set of indices, the way to state that s indexes a linearly independent subcollection is LinearIndependent R (fun x : ↥s ↦ (f x : W)) or similar. #21799 introduced a definition LinearIndepOn, which gives an alternative spelling LinearIndepOn R f s instead of LinearIndependent R (fun x : ↥s ↦ (f x : W)) for the indexed version, and (therefore) LinearIndepOn R id s for the set version. This PR updates spellings throughout mathlib, changing terms of type LinearIndependent R (Subtype.val : ↥s → W) to LinearIndepOn R id s and LinearIndependent R (fun x : ↥s ↦ (f x : W)) to LinearIndepOn R f s. The API using the old spellings has been deprecated, and replaced with new one - the diff is designed to be as small as possible subject to deprecating the old spellings. In some cases, where no extra work was needed, we generalized lemmas that previously apply to LinearIndepOn R id s to LinearIndepOn R v s for arbitrary v. But there is room to do this further in other places, some of which have been marked TODO. Most changes happen in LinearAlgebra/LinearIndependent.lean, but only about 100 lines have been added to the length, many of which are deprecated alias lines. Nearly all other changes are knock-on effects, where statements, proofs and (in two cases) definitions that use the old spellings are updated. 22 files are affected, but the majority only in the form of slight modifications of proofs to avoid deprecated lemmas. The two files other than LinearIndependent.lean with changed definitions are:

• Mathlib/LinearAlgebra/Dimension/Basic.lean (definition of Module.rank)
• Mathlib/LinearAlgebra/Dimension/RankNullity.lean (changed structure field of HasRankNullity) The files with changed theorem statements are:
• Mathlib/FieldTheory/Fixed.lean
• Mathlib/LinearAlgebra/Basis/VectorSpace.lean
• Mathlib/LinearAlgebra/Dimension/Constructions.lean
• Mathlib/LinearAlgebra/Dimension/Finite.lean
• Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
• Mathlib/LinearAlgebra/Dimension/LinearMap.lean
• Mathlib/LinearAlgebra/Dimension/Localization.lean
• Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean Zulip discussion