mathlib

faf106a3 - refactor(data/real/{e,}nnreal): reuse generic lemmas (#5751)

refactor(data/real/{e,}nnreal): reuse generic lemmas (#5751) * reuse `div_eq_mul_inv` and `one_div` from `div_inv_monoid`; * reuse lemmas about `group_with_zero` instead of repeating them in the `nnreal` namespace; * add `has_sum.div_const`.