Pi instances

Stream: maths

[Nicolò Cavalleri]

It seems that if I have [∀ x, normed_space 𝕜 (E x)] lean does not find and instance of [∀ x, module 𝕜 (E x)]. Does this mean I have to redeclare the instance hierarchy for pi instances? Or am I doing something wrong? In case yes, is there a trick?

[Eric Wieser]

This sounds similar to the problem we've been seeing with dfinsupp which also has this type of instance argument. Can you give a MWE?

[Kevin Buzzard]

import analysis.normed_space.basic

variables {𝕜 : Type} [normed_field 𝕜]
  {E : Type → Type} [∀ x, normed_group (E x)]

variable [∀ x, normed_space 𝕜 (E x)]


example : ∀ x, module 𝕜 (E x) := infer_instance
-- works fine for me