Commit 2021-12-15 17:00 930ae468

chore(analysis/special_functions/pow): remove duplicate lemmas concerning monotonicity of rpow (#10794) The lemmas rpow_left_monotone_of_nonneg and rpow_left_strict_mono_of_pos were duplicates of monotone_rpow_of_nonneg and strict_mono_rpow_of_pos, respectively. The duplicates are removed as well as references to them in mathlib in measure_theory/function/{continuous_function_dense, lp_space}