Stream: new members
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
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: May 11 2021 at 22:14 UTC