Commit 2025-05-25 09:55 5e80da41

View on Github →

fix(Order/Field/Pointwise): use * in the RHS (#25047) We may want to go back to smul in the future, if we generalize these lemmas to OrderedSMul.

Estimated changes

modified theorem LinearOrderedField.smul_Icc
modified theorem LinearOrderedField.smul_Ici
modified theorem LinearOrderedField.smul_Ico
modified theorem LinearOrderedField.smul_Iic
modified theorem LinearOrderedField.smul_Iio
modified theorem LinearOrderedField.smul_Ioc
modified theorem LinearOrderedField.smul_Ioi
modified theorem LinearOrderedField.smul_Ioo