Theorem LinearMap.ofClass_injective

Modification history

2026-09-08 10:36
Mathlib/Algebra/Module/LinearMap/Defs.lean
chore: rename SemilinearMapClass.semilinearMap to LinearMap.ofClass (#43376) …
Added LinearMap.ofClass_injectiveView on Github →