Theorem FixedDetMatrices.reduce_reduceStep

Modification history

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