Theorem LinearMap.coe_ofClass

Modification history

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