Theorem Algebra.lsmul_eq_smul_one

Modification history