Theorem PerfectPairing.finrank_eq

Modification history

2024-11-28 16:12
Mathlib/LinearAlgebra/PerfectPairing.lean
feat: drop finite-dimensionality assumption from `PerfectPairing.restrictScalarsField` (#18940)
Added PerfectPairing.finrank_eqView on Github →