Theorem LinearMap.coe_sum

Modification history

2025-11-26 19:12

Mathlib/Algebra/Module/Submodule/LinearMap.lean

chore: rename LinearMap.coeFn_sum to LinearMap.coe_sum (#32054)

Added LinearMap.coe_sum View on Github →