Def LinearMap.ofClass

Modification history

2026-09-08 10:36

Mathlib/Algebra/Module/LinearMap/Defs.lean

chore: rename SemilinearMapClass.semilinearMap to LinearMap.ofClass (#43376) …

Added LinearMap.ofClass View on Github →