Commit 2026-01-23 16:59 c99f0410

feat(LinearAlgebra/Transvection): the determinant of a transvection is equal to 1. (#32757) Prove that the determinant of a transvection is equal to 1 The proof goes by showing that the determinant of LinearMap.transvection f v is 1 + f v (even if f v is nonzero). I first treat the case of a field, distinguishing whether f v = 0 (so that we get a transvection) or not (so that we have a dilation). Then, by base change to the field of fractions, I can handle the case of a domain. Finally, the general case is treated by base change from the “universal case” where the base ring is the ring of polynomials in $$2n$$ indeterminates corresponding to the coefficients of $$f$$ and $$v$$.