Theorem lcm_eq_normalize

Modification history