mathlib

e73ac940 - feat (analysis/normed_space/lp_space):add l_infinity ring instances (#14104)

feat (analysis/normed_space/lp_space):add l_infinity ring instances (#14104) We define pointwise multiplication on `lp E ∞` and give it has_mul, non_unital_ring, non_unital_normed_ring, ring, normed_ring, comm_ring and normed_comm_ring instances under the appropriate assumptions. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>