Theorem LinearOrderedField.smul_Iio

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_IioView on Github →
2024-12-25 13:01
Mathlib/Algebra/Order/Field/Pointwise.lean
chore(Order/Field/Pointwise): golf (#20226) …
Modified LinearOrderedField.smul_IioView on Github →
2024-09-26 00:42
Mathlib/Algebra/Order/Field/Pointwise.lean
chore: split Algebra.Bounds and Algebra.Order.Pointwise (#16986) …
Modified LinearOrderedField.smul_IioView on Github →
2023-01-13 18:56
Mathlib/Algebra/Order/Pointwise.lean
feat: port Algebra.Order.Pointwise (#1533)
Added LinearOrderedField.smul_IioView on Github →