simple_func_dense_lp): generalize typeclasses (#19111)

Commit

2 years ago

chore(measure_theory/function/simple_func_dense_lp): generalize typeclasses (#19111) Lemmas like `to_Lp_smul` now apply for `normed_ring`s, not just `normed_field`s.

Author

eric-wieser

Parents

0b7c740e

mathlib3 5a2df4cd - chore(measure_theory/function/simple_func_dense_lp): generalize typeclasses (#19111)

mathlib3
5a2df4cd - chore(measure_theory/function/simple_func_dense_lp): generalize typeclasses (#19111)