Mathlib v3 is deprecated. Go to Mathlib v4

Theorem has_compact_mul_support.exists_pos_le_norm

Modification history

2023-02-10 10:20
src/analysis/normed/group/basic.lean
feat(analysis/fourier): Riemann-Lebesgue lemma (part 1) (#18361) …
Added has_compact_mul_support.exists_pos_le_normView on Github →