Theorem LinearOrderedField.smul_Ioo
Modification history
2025-05-25 09:55
Mathlib/Algebra/Order/Field/Pointwise.lean
fix(Order/Field/Pointwise): use `*` in the RHS (#25047) …
Modified LinearOrderedField.smul_IooView on Github →2024-12-25 13:01
Mathlib/Algebra/Order/Field/Pointwise.lean
chore(Order/Field/Pointwise): golf (#20226) …
Modified LinearOrderedField.smul_IooView on Github →