Theorem Filter.BoundedAtFilter.mul_zeroAtFilter

Modification history

2026-05-01 08:23
Mathlib/Order/Filter/ZeroAndBoundedAtFilter.lean
feat(NumberTheory/ModularForms): dimension formula for level one modular forms (#37979) …
Added Filter.BoundedAtFilter.mul_zeroAtFilterView on Github →