Theorem LinearEquiv.det_eq_one

Modification history

2026-01-24 12:29

Mathlib/LinearAlgebra/Transvection.lean

chore(LinearAlgebra/Transvection): adjust namespace (#34365) …

Deleted LinearEquiv.det_eq_one View on Github →

2026-01-23 16:59

Mathlib/LinearAlgebra/Transvection.lean

feat(LinearAlgebra/Transvection): the determinant of a transvection is equal to 1. (#32757) …

Added LinearEquiv.det_eq_one View on Github →