Theorem LinearEquiv.toLinearMap_eq_ofClass

Modification history

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