Theorem LinearOrderedField.smul_Ici

Modification history