Real functions as vector spaces

Stream: new members

[Icaro Costa]

I would like to define two real functions f and g and a real scalar a such that:

(af+g)(x) = a*f(x) + g(x)

I just tried to define them as follows

/-Function definitions-/
def f : ℝ → ℝ := sorry
def u : ℝ → ℝ := sorry

But Lean struggles to understand what I mean when I type a*f.

[Junyan Xu]

a • f for scalar multiplication. Both operands of multiplication * are always of the same type.

[Icaro Costa]

Junyan Xu said:

a • f for scalar multiplication. Both operands of multiplication * are always of the same type.

How do I type this symbol on VS code? Is it \dot?

[Eric Rodriguez]

\cdot, \bub are two options. You can hover over weird symbols to figure out how to type them.

[Icaro Costa]

Eric Rodriguez said:

\cdot, \bub are two options. You can hover over weird symbols to figure out how to type them.

Ok, thanks

[Eric Wieser]

\smul is what I usually type, since it builds muscle memory for finding the lemmas about it that call it smul

[Kevin Buzzard]

Wooah I always type \bub because it's shorter, but can confirm that even at my age it's very easy to know that it's called smul in lemmas

[Yaël Dillies]

\sm is enough to get it. No need to type the entire word

[Mario Carneiro]

\bu also works