Theorem FixedDetMatrix.smul_coe

Modification history

2024-12-13 07:53
Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
feat: representatives for the `FixedDetMatrices` under SL action (#16160) …
Deleted FixedDetMatrix.smul_coeView on Github →
2024-10-28 15:32
Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
feat: matrices with fixed determinant (#16159) …
Added FixedDetMatrix.smul_coeView on Github →