Zulip Chat Archive

Stream: general

Topic: Failed to synthesize ...


Heather Macbeth (May 24 2020 at 03:03):

What am I doing wrong here?

import analysis.normed_space.operator_norm

variables {𝕜 : Type*} [normed_field 𝕜]
variables {E : Type*} [normed_group E] [normed_space 𝕜 E]
variables {F : Type*} [normed_group F] [normed_space 𝕜 F]
variables {G : Type*} [normed_group G] [normed_space 𝕜 G]

#check E L[𝕜] (F L[𝕜] G)

gives the error "failed to synthesize type class instance for ... ⊢ topological_space (F →L[𝕜] G)".

Heather Macbeth (May 24 2020 at 03:03):

I would have thought that Lean could infer a topological space structure on F →L[𝕜] G, because (1) in analysis.normed_space.operator_norm we have

instance to_normed_space : normed_space 𝕜 (E L[𝕜] F)

(2) in analysis.normed_space.basic we have, for [normed_space α E],

instance normed_space.topological_vector_space : topological_vector_space α E

(3) in topology.algebra.module we have

abbreviation topological_vector_space (R : Type u) (M : Type v) [field R] [topological_space R]
[topological_space M] [add_comm_group M] [module R M]

Yury G. Kudryashov (May 24 2020 at 03:26):

Does to_normed_space need a nondiscrete_normed_field?

Heather Macbeth (May 24 2020 at 03:29):

Wow, I would never have caught that. Thank you, Yury!

Yury G. Kudryashov (May 24 2020 at 03:29):

BTW, could you please rename to_normed_space in section normed_algebra to normed_algebra.to_normed_space?

Heather Macbeth (May 24 2020 at 03:31):

Sure.


Last updated: Dec 20 2023 at 11:08 UTC