Theorem MulOpposite.finrank

Modification history

2025-07-23 11:19
Mathlib/LinearAlgebra/Basis/MulOpposite.lean
feat(LinearAlgebra/Basis/MulOpposite): basis of an opposite space (#25949) …
Added MulOpposite.finrankView on Github →