Commit 2026-05-14 02:57 ef1d0e44

View on Github →

feat: notation for composition of continuous semilinear maps (#39345)

Estimated changes

Modified Mathlib/Topology/Algebra/Module/LinearMap.lean

modified theorem ContinuousLinearMap.coe_comp'

modified theorem ContinuousLinearMap.comp_apply

modified theorem ContinuousLinearMap.comp_id

modified theorem ContinuousLinearMap.comp_zero

modified theorem ContinuousLinearMap.id_comp

modified theorem ContinuousLinearMap.mul_def

modified theorem ContinuousLinearMap.zero_comp