## Stream: new members

### Topic: Dangerous instance vs elaboration problems

#### Frédéric Dupuis (Sep 19 2020 at 03:28):

In #4057 (which defines inner products based on is_R_or_C), the main outstanding issue is that the linter reports a dangerous instance in the definition:

class inner_product_space (𝕜 : Type*) (α : Type*)
[nondiscrete_normed_field 𝕜] [normed_algebra ℝ 𝕜] [is_R_or_C 𝕜]
extends normed_group α, normed_space 𝕜 α, has_inner 𝕜 α := sorry


which presumably comes from the fact that normed_group α doesn't have 𝕜 as a parameter. I gather that the usual way to fix this is to move normed_group α into the assumptions, as in

class inner_product_space (𝕜 : Type*) (α : Type*)
[nondiscrete_normed_field 𝕜] [normed_algebra ℝ 𝕜] [is_R_or_C 𝕜]  [normed_group α]
extends normed_space 𝕜 α, has_inner 𝕜 α := sorry


However, when I do that, 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.

So: just how dangerous is an instance like this? Would it still send the search algorithm into a wild goose chase, even though the only possibilities for 𝕜 should always remain only ℂ and ℝ?

#### Heather Macbeth (Sep 19 2020 at 15:58):

I think you could have asked this in #maths! :) @Yury G. Kudryashov @Sebastien Gouezel ?

Last updated: May 13 2021 at 06:15 UTC