[Merged by Bors] - refactor(LinearIndependent): refactor to use LinearIndepOn

[apnelson1]

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

---

[github-actions]

PR summary e9c9122503

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ LinearIndepOn.comp_of_image
+ LinearIndepOn.extend
+ LinearIndepOn.extend_subset
+ LinearIndepOn.id_image
+ LinearIndepOn.id_imageₛ
+ LinearIndepOn.id_singleton
+ LinearIndepOn.id_union
+ LinearIndepOn.image
+ LinearIndepOn.image_of_comp
+ LinearIndepOn.injOn
+ LinearIndepOn.insert
+ LinearIndepOn.linearIndepOn_extend
+ LinearIndepOn.linearIndependent
+ LinearIndepOn.linearIndependent_restrict
+ LinearIndepOn.map_injOn
+ LinearIndepOn.ne_zero
+ LinearIndepOn.of_comp
+ LinearIndepOn.of_subsingleton
+ LinearIndepOn.singleton
+ LinearIndepOn.span_extend_eq_span
+ LinearIndepOn.subset_extend
+ LinearIndepOn.subset_span_extend
+ LinearIndepOn.union_of_quotient
+ LinearIndependent.linearIndepOn
+ LinearIndependent.linearIndepOn_id
+ LinearIndependent.linearIndepOn_id'
+ LinearIndependent.of_linearIndepOn_id_range
+ LinearIndependent.of_linearIndepOn_range
+ LinearMap.linearIndepOn_iff_of_injOn
+ eq_of_linearIndepOn_id_of_span_subtype
+ exists_linearIndepOn_id_extension
+ exists_linearIndepOn_of_lt_rank
+ exists_maximal_linearIndepOn
+ exists_maximal_linearIndepOn'
+ exists_of_linearIndepOn_of_finite_span
+ linearDepOn_iff
+ linearDepOn_iff'
+ linearDepOn_iff'ₛ
+ linearDepOn_iffₛ
+ linearIndepOn_biUnion_of_directed
+ linearIndepOn_equiv
+ linearIndepOn_iUnion_of_directed
+ linearIndepOn_id_iUnion_finite
+ linearIndepOn_id_insert
+ linearIndepOn_id_pair
+ linearIndepOn_id_range_iff
+ linearIndepOn_iff
+ linearIndepOn_iff_disjoint:
+ linearIndepOn_iff_image
+ linearIndepOn_iff_linearCombinationOn
+ linearIndepOn_iff_linearCombinationOnₛ
+ linearIndepOn_iffₛ
+ linearIndepOn_insert
+ linearIndepOn_of_finite
+ linearIndepOn_range_iff
+ linearIndepOn_sUnion_of_directed
+ linearIndependent_comp_subtype_iff
+ linearIndependent_set_coe_iff
+ linearIndependent_subtype_iff
+++- _
- LinearIndependent.coe_range
- LinearIndependent.extend_subset
- LinearIndependent.image
- LinearIndependent.image_of_comp
- LinearIndependent.image_subtypeₛ
- LinearIndependent.linearIndependent_extend
- LinearIndependent.span_extend_eq_span
- LinearIndependent.subset_extend
- LinearIndependent.subset_span_extend
- eq_of_linearIndependent_of_span_subtype
- exists_linearIndependent_of_lt_rank
- exists_maximal_independent
- exists_maximal_independent'
- exists_of_linearIndependent_of_finite_span
- linearIndependent_biUnion_of_directed
- linearIndependent_iUnion_finite_subtype
- linearIndependent_iUnion_of_directed
- linearIndependent_iff_linearCombinationOnₛ
- linearIndependent_sUnion_of_directed
- linearIndependent_set_subtype
- linearIndependent_singleton

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[j-loreaux]

Thanks @apnelson1 ! I think this is quite nice. I really appreciate the work you did here and in the creation of LinearIndepOn. I'm going to leave it just a bit longer in case anyone else has something to say, but if, after addressing these minor issues below, it's not merged in a few days, I'll come back to do it.

[Vierkantor]

This is some nice work, I'm happy to redo my split of LinearIndependent.lean so that this can be merged first in peace. :)

[apnelson1]

This is some nice work, I'm happy to redo my split of LinearIndependent.lean so that this can be merged first in peace. :)

Thanks for the review and the patience!

[j-loreaux]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style