feat(LinearAlgebra/Transvection/Generation): prove exceptional case in Dieudonné's theorem

[AntoineChambert-Loir]

Establish the fourth part of Dieudonné's theorem: is a linear equivalence is exceptional, it
is the product of finrank K (V ⧸ e.fixedSubmodule) transvections and one dilatransvection.

---

• depends on: feat(LinearAlgebra/Transvection): characterization of transvections among dilatransvections #33348
• depends on: feat(LinearAlgebra/Transvection/Basic): define dilatransvections #33347
• 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

[github-actions]

PR summary d68c4dc09f

Import changes for modified files

Dependency changes

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

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.Transvection	-1390
Mathlib.LinearAlgebra.Transvection.Basic (new file)	1366
Mathlib.LinearAlgebra.Center (new file)	1367
Mathlib.LinearAlgebra.Transvection.Generation (new file)	1368

---

Declarations diff

+ IsBaseChange.transvection
+ IsExceptional
+ IsExceptional.mem_mul_transvections_pow_mul_dilatransvections
+ 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
+ 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_sup_span_singleton
+ fixedReduce
+ fixedReduce_eq_one
+ fixedReduce_eq_smul_iff
+ 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
+ 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_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_of_not_isExceptional
+ 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_of_fixedReduce_eq_one
+ mem_transvections_pow_mul_dilatransvections_of_fixedReduce_ne_smul_id
+ one_mem_dilatransvections
+ one_mem_transvections
+ reduce
+ reduce_mk
+ reduce_mkQ
+ restrict
+ smul_submodule_def
+ subgroup_closure_dilatransvections_eq_top
+ sup_span_eq_top
+ 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): characterization of transvections among dilatransvections #33348
• feat(LinearAlgebra/Transvection/Basic): define dilatransvections #33347
• 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
  By Dependent Issues (🤖). Happy coding!