feat(LinearAlgebra/Transvection/Generation): a linear equivalence is the product of dilatransvections

[AntoineChambert-Loir]

Prove that a linear equivalence e is the product of V ⧸ e.fixedSubmodule dilatransvections.
(It cannot be a product of less.)

---

• depends on: feat(LinearAlgebra/Transvection/Basic): define dilatransvections #33347
• depends on: feat(LinearAlgebra/Transvection): characterization of transvections among dilatransvections #33348
• depends on: chore(LinearAlgebra/Transvection/Basic): mv Transvection.lean file to Transvection.Basic.lean #33387
• depends on: feat(LinearAlgebra/Center): description of the center of the algebra of endomorphisms #33282
• depends on: feat(LinearAlgebra/Transvection/Generation): non-exceptional case in Dieudonné's theorem #33392
•  depends on: feat(LinearAlgebra/Transvection/Generation): prove exceptional case in Dieudonné's theorem #33402
•  depends on: feat(LinearAlgebra/Transvection/Generation): prove the third part of Dieudonné's theorem #33485

[github-actions]

PR summary cb3ccde1ed

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.LinearAlgebra.Transvection	1408	0	-1408 (-100.00%)

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.Transvection	-1408
Mathlib.LinearAlgebra.Transvection.Basic (new file)	1370
Mathlib.LinearAlgebra.Center (new file)	1371
Mathlib.LinearAlgebra.Transvection.Generation (new file)	1373

---

Declarations diff

+ Finset.iInf_univ
+ IsBaseChange.transvection
+ IsExceptional
+ LinearEquiv.transvection.baseChange
+ LinearIndependent.pair_smul_smul_iff
+ LinearMap.transvection.baseChange
+ _root_.Module.Free.of_det_ne_one
+ closure_pow_le
+ coe_restrict
+ commute_transvections_iff_of_basis
+ comp_smul_smul
+ dilatransvection
+ dilatransvection.apply
+ dilatransvection.coe_toLinearMap
+ dilatransvection_mem_dilatransvections
+ dilatransvections
+ dilatransvections_pow_mono
+ eq_top_iff_finrank_eq
+ exists_eq_smul_id_of_forall_notLinearIndependent
+ exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent
+ exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis
+ finrank_fixedSubmodule_add_le
+ finrank_fixedSubmodule_dilatransvection_mul_le
+ finrank_fixedSubmodule_mul_dilatransvection_le
+ finrank_le_one_add_finrank_fixedSubmodule_dilatransvection
+ finrank_quotient_fixedSubmodule_of_mem_dilatransvections_pow
+ finrank_quotient_iInf_le_sum_finrank_quotient
+ finrank_quotient_inf_le_finrank_quotient_add_finrank_quotient
+ finrank_quotient_inf_le_finrank_quotient_add_finrank_quotient'
+ finrank_sup_span_singleton
+ fixedReduce
+ fixedReduce_eq_one
+ fixedReduce_eq_smul_iff
+ fixedReduce_mem_dilatransvections_pow
+ fixedReduce_mem_transvections_mul_dilatransvections_pow
+ fixedReduce_mem_transvections_pow_mul_dilatransvections
+ fixedReduce_mk
+ fixedReduce_mkQ
+ fixedSubmodule
+ fixedSubmodule_eq_ker
+ fixedSubmodule_eq_top_iff
+ fixedSubmodule_mul_inf_fixedSubmodule_le_fixedSubmodule
+ fixedSubmodule_mul_inf_fixedSubmodule_le_fixedSubmodule'
+ fixedSubmodule_transvection_mul
+ fixingSubgroup_le_stabilizer
+ iInf_fixedSubmodule_le_fixedSubmodule_prod
+ inf_fixedSubmodule_le_fixedSubmodule_mul
+ inv_mem_dilatransvections_iff
+ inv_mem_transvections_iff
+ ker_le_fixedSubmodule_transvection
+ le_one_add_finrank_fixedSubmodule_dilatransvection_mul
+ le_one_add_finrank_fixedSubmodule_dilatransvection_mul'
+ le_one_add_finrank_fixedSubmodule_mul_dilatransvection
+ map_eq_of_mem_fixingSubgroup
+ mem_center_of_apply_eq_smul
+ mem_dilatransvections_iff_finrank
+ mem_dilatransvections_iff_finrank_quotient
+ mem_dilatransvections_iff_rank
+ mem_dilatransvections_iff_rank_quotient
+ mem_dilatransvections_pow
+ mem_fixedSubmodule_iff
+ mem_fixedSubmodule_transvection_iff
+ mem_stabilizer_fixedSubmodule
+ mem_stabilizer_submodule
+ mem_stabilizer_submodule_iff_map_eq
+ mem_stabilizer_submodule_of_le_fixedSubmodule
+ mem_transvections
+ mem_transvections_iff
+ mem_transvections_iff'
+ mem_transvections_pow_mul_dilatransvections
+ mem_transvections_pow_mul_dilatransvections_of_fixedReduce_eq_one
+ mem_transvections_pow_mul_dilatransvections_of_fixedReduce_ne_smul_id
+ mem_transvections_pow_mul_dilatransvections_of_notIsExceptional
+ notIsExceptional_of_mem_transvections_mul_dilatransvections_pow
+ notIsExceptional_of_mem_transvections_pow_mul_dilatransvections
+ not_mem_transvections_mul_dilatransvections_pow
+ one_mem_dilatransvections
+ one_mem_transvections
+ reduce
+ reduce_mem_dilatransvections
+ reduce_mem_transvections
+ reduce_mk
+ reduce_mkQ
+ restrict
+ smul_submodule_def
+ subgroup_closure_dilatransvections_eq_top
+ sup_span_eq_top
+ symm_apply
+ transvection_mem_dilatransvections
+ transvection_mem_transvections
+ transvections
+ transvections_pow_mono
+ transvections_subset_dilatransvections
- _root_.IsBaseChange.transvection
- _root_.LinearEquiv.transvection.baseChange
- baseChange

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

---

note: file Mathlib/LinearAlgebra/Transvection.lean was removed.
Please create a follow-up pull request adding a module deprecation. Thanks!

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(LinearAlgebra/Transvection/Basic): define dilatransvections #33347
• feat(LinearAlgebra/Transvection): characterization of transvections among dilatransvections #33348
• chore(LinearAlgebra/Transvection/Basic): mv Transvection.lean file to Transvection.Basic.lean #33387
• feat(LinearAlgebra/Center): description of the center of the algebra of endomorphisms #33282
• feat(LinearAlgebra/Transvection/Generation): non-exceptional case in Dieudonné's theorem #33392
• feat(LinearAlgebra/Transvection/Generation): prove exceptional case in Dieudonné's theorem #33402
• feat(LinearAlgebra/Transvection/Generation): prove the third part of Dieudonné's theorem #33485
  By Dependent Issues (🤖). Happy coding!