mathlib3

46b633fd - refactor(analysis/inner_product_space/basic): do not extend normed_add_comm_group (#18583)

refactor(analysis/inner_product_space/basic): do not extend normed_add_comm_group (#18583) This replaces `[inner_product_space K V]` with `[normed_add_comm_group V] [inner_product_space K V]`. Before this PR, we had `inner_product_space K V extends normed_add_comm_group V`. At first glance this is a rather strange arrangement; we certainly don't have `module R V extends add_comm_group V`. The argument usually goes that `Derived A B extends Base B` is unsafe, because the `Derived.toBase` instance has no way of knowing which `A` to look for. For `inner_product_space K V` we argued that this problem doesn't apply, as `is_R_or_C K` means that in practice there are only two possible values of `K`. This is indeed enough to stop typeclass search grinding to a halt. The motivation for the old design is described by @dupuisf [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Dangerous.20instance.20vs.20elaboration.20problems/near/210594971): > However, when I do (the contents of this PR), I run into some very annoying elaboration issues where I have to constantly spoonfeed it `𝕜` and/or `α` in lemmas that rewrite norms in terms of inner products, even though the relevant instance is directly present in the context. While it may ease elaboration issues, there are a number of new problems that `inner_product_space K V extends normed_add_comm_group V` causes: 1. It is confusing when compared to all other typeclasses. After being told to write ```lean variables [add_comm_group U] [module R U] variables [normed_add_comm_group V] [normed_space R V] ``` it is natural to assume that the inner product space version would be ```lean variables [normed_add_comm_group W] [inner_product_space K W] ``` But writing this leads to `W` having two unrelated addition operations! 2. It doesn't allow a space `W` to be an inner product space over both R and C. For a (normed) module, you can write ```lean variables [add_comm_group U] [module R U] [module C U] variables [normed_add_comm_group V] [normed_space R V] [normed_space C V] ``` but writing `[inner_product_space R W] [inner_product_space C W]` again puts two unrelated `+` operators on `V` 3. It doesn't compose with other normed typeclasses. We can talk about a (normed) module with multiplication as ```lean variables [ring U] [module R U] variables [normed_ring V] [normed_space K V] ``` but once again, typing `[normed_ring W] [inner_product_space K W]` gives us two unrelated `+` operators. This prevents us generalizing over `real`, `complex`, and `quaternion`. We could work around this by defining variants of `inner_product_space` for `normed_ring A`, `normed_comm_ring A`, `normed_division_ring A`, `normed_field A`, but this doesn't scale well. If we do things "the module way" then we only need one new typeclass instead of four, ```lean class inner_product_algebra (K A) [is_R_or_C K] [normed_ring A] extends normed_algebra K A, inner_product_space K A ``` 5. The "`is_R_or_C` makes it OK" argument stops working if we generalize to [quaternionic inner product spaces](https://link.springer.com/chapter/10.1007/978-94-009-3713-0_13) The majority of this PR is adding `[normed_add_comm_group _]` to every `variables` line about `inner_product_space`. The rest is specifying the scalar manually where previously unification would find it for us. [This Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/inner_product_space.20and.20normed_algebra/near/341848831) has some initial discussion about this change.