[Merged by Bors] - refactor(*): move normed field lemmas into root namespace

[j-loreaux]

This takes the normed field lemmas given in analysis.normed_space.basic and moves them from the normed_field namespace into the root namespace.

This PR moves these lemmas and definitions: norm_mul, nnnorm_mul, norm_hom, nnnorm_hom, norm_pow, nnnorm_pow, norm_prod, nnnorm_prod, norm_div, nnnorm_div, norm_inv, nnnorm_inv, norm_zpow, nnnorm_zpow.

---

[j-loreaux]

As discussed here on Zulip, these lemmas should be moved to the root namespace. This was originally attempted as part of #12132 which introduces normed division rings and generalized most of these lemmas to that setting, but I ran into build issues. So it was suggested to split it into two PRs.

[urkud]

Could you please list all theorems that you move to the root ns?

[urkud]

I'm not sure that exists_norm_lt should go to the root ns. There is a version of this lemma for a non-trivial normed space.

[j-loreaux]

The following are the lemmas moved into the root namespace. I could see moving the instances and the last 6 lemmas back into normed_field. Thoughts? (Edit: updated list. strike out means it is kept in the normed_field namespace.)

norm_mul
to_normed_comm_ring (instance)
to_norm_one_class (instance)
nnnorm_mul
norm_hom
nnnorm_hom
norm_pow
nnnorm_pow
norm_prod
nnnorm_prod
norm_div
nnnorm_div
norm_inv
nnnorm_inv
norm_zpow
nnnorm_zpow
exists_one_lt_norm
exists_norm_lt_one
exists_lt_norm
exists_norm_lt
punctured_nhds_ne_bot
nhds_within_is_unit_ne_bot

[eric-wieser]

The instances definitely belong inside the namespace

[eric-wieser]

I'm not sure that exists_norm_lt should go to the root ns. There is a version of this lemma for a non-trivial normed space.

I can't find that lemma - can you give the full name?

[j-loreaux]

I think he intends : normed_space.exists_lt_norm

[eric-wieser]

Can normed_field.exists_lt_norm be proved with normed_space.exists_lt_norm?

[j-loreaux]

It goes in the reverse direction. You use the field version to prove the normed space version.

[urkud]

We can have the normed_space versions in the root namespace. Then we either call normed_field.exists... k or exists... k k.

[urkud]

BTW, I think that we should have exists_lt_norm (r : real) (...) : ∃ c : k, r < norm c, not exists_one_lt_norm.

[j-loreaux]

@urkud normed_space.exists_lt_norm is the only normed space version we have (I think). Are you saying you want me to add more versions corresponding to the normed_field ones?

[urkud]

I think that for now, you can just leave these lemmas in the normed_field NS.

[urkud]

Thanks!
bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests