[Merged by Bors] - feat(normed_space/inner_product): euclidean_space.norm_eq

[pechersky]

---

[hrmacbeth]

Can we try to do this by fixing the diamond?
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.60inner_product_space.20.E2.84.9D.20(euclidean_space.20.F0.9D.95.9C.20n).60.3F

I think that's the more natural approach.

[pechersky]

I'm only adding the lemma that expands out the norm for a term of the euclidean space. I think fixing the diamond might have to do with how the semimodules are defined differently on the different type wrappers.

[hrmacbeth]

Ah, I see. Can you please give this lemma for pi_Lp 2 one_le_two, similar to pi_Lp.inner_apply, and deduce the euclidean_space version from it? (At that point the euclidean_space version may not even be needed, since it is definitionally a pi_Lp.)

[pechersky]

I added this lemma because of the notational confusion between ^ when encoding rpow or monoid.pow. For working with nat powers, this will allow for cleaner rewrites, with easy discharging with norm_num. I couldn't figure out how to use . tactic.norm_num as the out_param there.

[hrmacbeth]

I added this lemma because of the notational confusion between ^ when encoding rpow or monoid.pow. For working with nat powers, this will allow for cleaner rewrites, with easy discharging with norm_num. I couldn't figure out how to use . tactic.norm_num as the out_param there.

This seems reasonable to me, but I'd like someone like @sgouezel who's been involved in the design of the L^p spaces to decide about this, in case there's a reason we haven't had lemmas like this already.

[sgouezel]

bors r+
Thanks!

[bors]

Pull request successfully merged into master.

Build succeeded:

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