Theorem Filter.EventuallyEq.fun_pow_const

Modification history

2026-03-16 05:13
Mathlib/Order/Filter/Basic.lean
feat(translate): support `to_additive (attr := to_fun)` (#36305) …
Deleted Filter.EventuallyEq.fun_pow_constView on Github →
2025-08-06 17:32
Mathlib/Order/Filter/Basic.lean
chore(Order/Filter/Basic): write lemmas in point-free style (#27184) …
Added Filter.EventuallyEq.fun_pow_constView on Github →