Theorem Filter.pure_smul

Modification history

2023-12-08 10:23

Mathlib/Order/Filter/Pointwise.lean

chore: Replace `(· op ·) a` by `(a op ·)` (#8843) …

Modified Filter.pure_smul View on Github →

2023-01-30 19:30

Mathlib/Order/Filter/Pointwise.lean

feat: port Order.Filter.Pointwise (#1839)

Added Filter.pure_smul View on Github →