inner product in a normed space

Stream: new members

[Mii Nguyen]

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]

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

[Scott Morrison]

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