## Stream: new members

### Topic: Real functions as vector spaces

#### Icaro Costa (Jan 13 2023 at 00:33):

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 (Jan 13 2023 at 00:34):

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

#### Icaro Costa (Jan 13 2023 at 00:37):

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 (Jan 13 2023 at 00:40):

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

#### Icaro Costa (Jan 13 2023 at 00:40):

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 (Jan 13 2023 at 00:43):

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

#### Kevin Buzzard (Jan 13 2023 at 07:43):

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 (Jan 13 2023 at 08:46):

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

#### Mario Carneiro (Jan 13 2023 at 08:46):

\bu also works

Last updated: Dec 20 2023 at 11:08 UTC