mathlib3

370cc484 - chore(data/real/nnreal): Golf (#16307)

chore(data/real/nnreal): Golf (#16307) Generalize various lemmas to `linear_ordered_semifield` or weaker so that they apply to `nnreal`. Golf the `nnreal` API using them.