Commit 2026-01-24 12:29 fc278a17

View on Github →

chore(LinearAlgebra/Transvection): adjust namespace (#34365) Adjust namespace for LinearEquiv.transvection.det_eq_one (was LinearEquiv.det_eq_one). A deprecation is probably useless since the lemma was added one day ago.

Estimated changes