feat(LinearAlgebra/Transvection): characterization of transvections among dilatransvections

[AntoineChambert-Loir]

WIP.

• LinearEquiv.fixedReduce. Pass a linear equivalence to the quotient by a fixed subspace.

• Characterize transvections among dilatransvections by the fact that their reduction is the identity.

---

• depends on: feat(LinearAlgebra/Transvection/Basic): define dilatransvections #33347

[github-actions]

PR summary d68c4dc09f

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.LinearAlgebra.Transvection	1390	1366	-24 (-1.73%)

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.Transvection	-24

---

Declarations diff

+ IsBaseChange.transvection
+ LinearEquiv.transvection.baseChange
+ LinearMap.transvection.baseChange
+ Submodule.sup_span_eq_top
+ _root_.Module.Free.of_det_ne_one
+ coe_restrict
+ dilatransvections
+ dilatransvections_pow_mono
+ 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'
+ fixingSubgroup_le_stabilizer
+ inf_fixedSubmodule_le_fixedSubmodule_mul
+ inv.mem_dilatransvections_iff
+ inv_mem_transvections_iff
+ ker_le_fixedSubmodule_transvection
+ map_eq_of_mem_fixingSubgroup
+ mem_dilatransvections_iff_finrank
+ mem_dilatransvections_iff_finrank_quotient
+ mem_dilatransvections_iff_rank
+ mem_dilatransvections_iff_rank_quotient
+ 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'
+ one_mem_dilatransvections
+ one_mem_transvections
+ reduce
+ reduce_mk
+ reduce_mkQ
+ restrict
+ smul_submodule_def
+ 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).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(LinearAlgebra/Transvection/Basic): define dilatransvections #33347
  By Dependent Issues (🤖). Happy coding!