Theorem FixedDetMatrices.reps_entries_le_m'

Modification history

2024-12-13 07:53
Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
feat: representatives for the `FixedDetMatrices` under SL action (#16160) …
Added FixedDetMatrices.reps_entries_le_m'View on Github →