Theorem LinearEquiv.transvection.det_eq_one

Modification history

2026-01-24 12:29
Mathlib/LinearAlgebra/Transvection.lean
chore(LinearAlgebra/Transvection): adjust namespace (#34365) …
Added LinearEquiv.transvection.det_eq_oneView on Github →