Commit 2026-01-26 08:43 2f629baf

feat(LinearAlgebra/Transvection/Basic): define dilatransvections (#33347) Define LinearEquiv.dilatransvections. These are linear equivalences whose associated linear map is a transvection. This definition has the interest of being usable without any assumption on the base ring. Over a division ring, they correspond exactly to those linear equivalences e such that e - LinearMap.id has rank at most one. They (will) appear in Dieudonné's theorem that describes the generation of elements of the general linear group as products of several transvections and one additional dilatransvection.