mathlib

48998760 - projections from product of modules are linear