# Zulip Chat Archive

## 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