mathlib4 feat(LinearAlgebra/Transvection): auxiliary lemmas to compute the determinant of transvection in a module

Auxiliary results towards the proof that the determinant of a transvection is equal to 1.

[x] depends on: #31164
[x] depends on: #31165
[x] depends on: #30987
[x] depends on: #31078
[x] depends on: #31162

Nov 01 '25 00:11 AntoineChambert-Loir

PR summary 493ca15820

Import changes exceeding 2%

%	File
+32.82%	`Mathlib.LinearAlgebra.Transvection`
+27.47%	`Mathlib.RingTheory.TensorProduct.IsBaseChangeHom`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.LinearAlgebra.Transvection	1045	1388	+343 (+32.82%)
Mathlib.RingTheory.TensorProduct.IsBaseChangeHom	1041	1327	+286 (+27.47%)

Import changes for all files

Files	Import difference
`Mathlib.LinearAlgebra.Dual.BaseChange`	284
`Mathlib.RingTheory.TensorProduct.IsBaseChangeHom`	286
`Mathlib.LinearAlgebra.Transvection`	343

Declarations diff

+ _root_.span_range_eq_top_iff_surjective_finsuppLinearCombination + coe_finsuppScalarRight' + det_endHom + endHom_comp + endHom_comp_apply + endHom_one + endHom_toMatrix + eq_id_of_finrank_le_one + finsuppScalarRight' + finsuppScalarRight_smul + free_of_det_ne_one + linearMapLeftRightHom_toMatrix + of_basis + of_fintype_basis + of_fintype_basis_eq + span_range_eq_top_iff_surjective_fintypeLinearCombination ++-- of_right_eq_zero +-+- apply +-+- transvection

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).

Nov 01 '25 00:11 github-actions[bot]

This pull request has conflicts, please merge master and resolve them.

Nov 10 '25 17:11 mathlib4-merge-conflict-bot

This pull request has conflicts, please merge master and resolve them.

Nov 16 '25 20:11 mathlib4-merge-conflict-bot

This pull request has conflicts, please merge master and resolve them.

Nov 19 '25 08:11 mathlib4-merge-conflict-bot

This pull request has conflicts, please merge master and resolve them.

Nov 28 '25 15:11 mathlib4-merge-conflict-bot

This pull request has conflicts, please merge master and resolve them.

Nov 30 '25 22:11 mathlib4-merge-conflict-bot

This pull request has conflicts, please merge master and resolve them.

Dec 01 '25 19:12 mathlib4-merge-conflict-bot

This PR/issue depends on:

~~leanprover-community/mathlib4#31164~~
~~leanprover-community/mathlib4#31165~~
~~leanprover-community/mathlib4#30987~~
~~leanprover-community/mathlib4#31078~~
~~leanprover-community/mathlib4#31162~~ By Dependent Issues (🤖). Happy coding!

Dec 08 '25 14:12 mathlib4-dependent-issues-bot

This pull request has conflicts, please merge master and resolve them.

Dec 08 '25 15:12 mathlib4-merge-conflict-bot

To make this easier to review, could you please open a separate PR with all the changes in all the files except the transvection file? The changes there are already +300, so ideally only those changes would end up as one PR. If the prerequisites are mutually independent, they can be several PRs.

Dec 10 '25 16:12 dagurtomas

What tool would you recommend to split the PR into those several pieces?

Dec 11 '25 11:12 AntoineChambert-Loir

I don't know of any tool... A hack you could use in this case is to branch of this PR's branch and remove the transvection file, and open a new PR from that branch

Dec 11 '25 18:12 dagurtomas

I note that the import increase affects only a leaf file LinearAlgebra.Transvection and a file imported only by a leaf LinearAlgebra.Dual.BaseChange so I think we can probably justify these import increases.

Dec 12 '25 16:12 ocfnash

This pull request has conflicts, please merge master and resolve them.

Dec 18 '25 11:12 mathlib4-merge-conflict-bot

Thanks both to author and reviewer!

bors merge

Dec 22 '25 17:12 ocfnash

Pull request successfully merged into master.

Build succeeded:

Dec 22 '25 20:12 mathlib-bors[bot]