Theorem Subspace.map_le_dualAnnihilator_dualAnnihilator

Modification history

2023-12-27 12:26
Mathlib/LinearAlgebra/Dual.lean
feat: OrderIso between finite-codimensional subspaces and finite-dimensional subspaces in the dual (#9124) …
Added Subspace.map_le_dualAnnihilator_dualAnnihilatorView on Github →