Theorem DirectSum.coe_decompose_mul_of_right_mem_of_le

Modification history