Zulip Chat Archive

Stream: new members

Topic: inner product in a normed space


Mii Nguyen (Aug 01 2019 at 11:15):

I recently try to include inner product to a normed space. Here is my work:

open normed_group

class has_inner_product (α : Type*) := (inner: α  α  )

export has_inner_product (inner)

local infix . := inner

structure inner_product (α : Type*)[normed_group α ] [normed_space  α]:=
(refx :  x y : α , x.y = y.x )
(add :  x y z : α , (x + y).z = x.z + y.z)
(mul :  k :  , x y : α , (k*x).y = k*(x.y))
(pos :  x : α , x.x  0)
(eq_zero:  x : α , x.x = 0  x = 0)
(norm :  x : α , x.x = x∥^2 )

the message error I have is :
invalid field notation, type is not of the form (C ...) where C is a constant
x
has type
α

I don't understand the error. Can you help me with this? Thank you.

Scott Morrison (Aug 01 2019 at 11:23):

I suspect your notation isn't working the way you expect, and Lean is still parsing the . as field notation.

Scott Morrison (Aug 01 2019 at 11:24):

It does seem a bit ambitious trying to overload ., given it has a built-in language meaning.


Last updated: Dec 20 2023 at 11:08 UTC