Theorem Filter.EventuallyEq.const_smul

Modification history

2024-01-16 07:51
Mathlib/Order/Filter/Basic.lean
feat(MeasureTheory/Function/StronglyMeasurable): pow lemmas (#9489) …
Deleted Filter.EventuallyEq.const_smulView on Github →
2023-01-23 08:16
Mathlib/Order/Filter/Basic.lean
Feat: port Order.Filter.Basic (#1750)
Added Filter.EventuallyEq.const_smulView on Github →