Theorem LinearMap.codRestrict₂_apply

Modification history

2024-11-07 11:59
Mathlib/Algebra/Module/Submodule/Equiv.lean
feat: define restrictions of perfect pairings (#18559) …
Added LinearMap.codRestrict₂_applyView on Github →