Naming inconsistencies

Stream: new members

[Gareth Ma]

Hi, not sure where to ask this so here I am. I am looking at the number_theory.padics.padic_numbers file, and inside two things defined that I am wondering about - padic_norm_e and the notation || ||. They are similar in that they essentially define the same thing: \u padic_norm_e n = || n ||. However, they also have different type signatures:padic_norm_e is an actual function that takes on rational values, while the || || is a real norm that takes on real values. Even worse, the function names seems to be very messed up. For example, docs#padic_norm_e.eq_of_norm_add_lt_left is an inequality on || ||, despite living in the namespace padic_norm_e. Do you guys think it is a problem, like is it inconsistent with mathlib naming conventions?

[Eric Wieser]

Those lemmas indeed look misnamed, I'd expect them in the padic namespace

[Gareth Ma]

Eric Wieser said:

Those lemmas indeed look misnamed, I'd expect them in the padic namespace

Screenshot-2023-02-15-at-13.47.29.png
Do you think this should be renamed to padic.norm_mul?

[Yaël Dillies]

I think it should be deleted given that we already have docs#norm_mul