Mathlib v3 is deprecated. Go to Mathlib v4

Theorem has_compact_mul_support.is_one_at_infty

Modification history

2023-02-10 10:20
src/topology/uniform_space/compact.lean
feat(analysis/fourier): Riemann-Lebesgue lemma (part 1) (#18361) …
Added has_compact_mul_support.is_one_at_inftyView on Github →