Theorem lie_nsmul

Modification history