Theorem LinearEquiv.ofInjective_symm_apply

Modification history

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