Commit 2022-07-01 10:20 e73ac940
View on Github →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.