Commit 2022-04-09 22:07 22b7d21f

feat(analysis/normed*): if f → 0 and g is bounded, then f * g → 0 (#13248) Also drop is_bounded_under_of_tendsto: it's just h.norm.is_bounded_under_le.