We prove the theorem of [Dieudonné-1955][J. Dieudonné, “Sur les générateurs
des groupes classiques”].

Let K be a division ring and V be a K-module.

• LinearEquiv.mem_transvections_pow_mul_dilatransvections_of_fixedReduce_eq_one:
  If e.fixedReduce = 1, then e can be written as the product
  of finrank K (V ⧸ e.fixedSubmodule) - 1 transvections
  and one dilatransvection.
  This is the first part of the non-exceptional case in Dieudonné's theorem.
  (This statement is not interesting when e = 1.)

• LinearEquiv.mem_transvections_pow_mul_dilatransvections_of_fixedReduce_ne_smul_id:
  If e.fixedReduce is not a homothety, then e can be written as the product
  of finrank K (V ⧸ e.fixedSubmodule) - 1 transvections and one dilatransvection.
  This is the second part of the non-exceptional case in Dieudonné's theorem.

• LinearEquiv.IsExceptional:
  A linear equivalence e : V ≃ₗ[K] V is exceptional if 1 < finrank K (V ⧸ e.fixedSubmodule)
  and if e.fixedReduce is a nontrivial homothety.

• LinearEquiv.mem_dilatransvections_pow_of_notIsExceptional:
  This is the non-exceptional case in Dieudonné's theorem,
  as a combination of the two preceding statements.

• depends on: [Merged by Bors] - feat(LinearAlgebra/Transvection): characterization of transvections among dilatransvections #33348
• depends on: [Merged by Bors] - feat(LinearAlgebra/Center): description of the center of the algebra of endomorphisms #33282
• depends on: [Merged by Bors] - feat(LinearAlgebra/Transvection/Basic): define dilatransvections #33347
• depends on: [Merged by Bors] - chore(LinearAlgebra/Transvection/Basic): move Transvection.lean file to Transvection.Basic.lean #33387