Theorem Filter.EventuallyConst.mulIndicator_const

Modification history

2026-10-13 14:51
Mathlib/Order/Filter/EventuallyConst.lean
refactor(Data): make `Set` a one-field structure (#41506) …
Modified Filter.EventuallyConst.mulIndicator_constView on Github →
2023-08-22 13:23
Mathlib/Order/Filter/EventuallyConst.lean
refactor(Filter/EventuallyConst): redefine (#6673)
Added Filter.EventuallyConst.mulIndicator_constView on Github →