Theorem tprod_tprod_eq_mulSingle

Modification history