mathlib

b91cdb91 - refactor(data/nnreal): rename nnreal.of_real to real.to_nnreal (#7750)

refactor(data/nnreal): rename nnreal.of_real to real.to_nnreal (#7750) I am in the middle of a project involving reals, nnreals, ennreals and ereals. There is a maze of coercions and maps between the 4 of them, with completely incoherent naming scheme (do you think that `measurable.nnreal_coe` is speaking of the coercion from `nnreal` to `real` or to `ennreal`, or of a coercion into `nnreal`? currently, it's for the coercion from `nnreal` to `real`, and the analogous lemma for the coercion from `nnreal` to `ennreal` is called `measurable.ennreal_coe`!). I'd like to normalize all this to have something coherent: * maps are defined from a type to another one, to be able to use dot notation. * when there are coercions, all lemmas should be formulated in terms of the coercion, and not of the explicit map * when there is an ambiguity, lemmas on coercions should mention both the source and the target (like in `measurable.coe_nnreal_real`, say). The PR is one first step in this direction, renaming `nnreal.of_real` to `real.to_nnreal` (which makes it possible to use dot notation).