# Zulip Chat Archive

## Stream: general

### Topic: Notation for span

#### Heather Macbeth (Dec 22 2020 at 23:18):

I would like to find some kind of notation for the span of a vector, really anything shorter than typing `span ℝ {v}`

repeatedly. Can someone help me troubleshoot? I have tried

```
import linear_algebra.basic
import data.real.basic
infix `∙`:1000 := λ 𝕜 x, submodule.span 𝕜 {x}
notation `⟪`x`⟫_`𝕜 := submodule.span 𝕜 {x}
variables {E : Type*} [add_comm_group E] [module ℝ E]
example (x y : E) (hy : y ∉ (ℝ ∙ x)) (hy' : y ≠ x) : y = 0 := sorry
example (x y : E) (hy : y ∉ ⟪x⟫_ℝ) (hy' : y ≠ x) : y = 0 := sorry
```

which give the errors, respectively,

```
failed to synthesize type class instance for
E : Type u_1,
_inst_1 : add_comm_group E,
_inst_2 : module ℝ E,
x y : E,
𝕜 : Type ?,
x : ?m_1
⊢ semiring 𝕜
```

(among others) and

```
don't know how to synthesize placeholder
context:
E : Type u_1,
_inst_1 : add_comm_group E,
_inst_2 : module ℝ E,
x y : E
⊢ Type ?
```

#### Heather Macbeth (Dec 22 2020 at 23:24):

(please ignore the dubious mathematics, I just want it to typecheck!)

#### Adam Topaz (Dec 22 2020 at 23:26):

This works:

```
import linear_algebra.basic
import data.real.basic
notation `⟪`x`⟫_`𝕜 := submodule.span 𝕜 (set.insert x ∅)
variables {E : Type*} [add_comm_group E] [module ℝ E]
example (x y : E) (hy : y ∉ ⟪ x ⟫_ℝ) (hy' : y ≠ x) : y = 0 := sorry
```

#### Adam Topaz (Dec 22 2020 at 23:27):

I feel like there was a similar issue with similar notation around adjoining elements to fields in the work around Galois theory, but I don't remember how it was resolved.

#### Adam Topaz (Dec 22 2020 at 23:27):

@Thomas Browning probably knows :)

#### Rob Lewis (Dec 22 2020 at 23:28):

`example (x y : E) (hy : y ∉ submodule.span ℝ {x}) (hy' : y ≠ x) : y = 0 := sorry`

doesn't work, no notation at all

#### Rob Lewis (Dec 22 2020 at 23:28):

It does seem to be because Lean doesn't pick up on `{x} : set E`

#### Adam Topaz (Dec 22 2020 at 23:29):

This also works:

```
import linear_algebra.basic
import data.real.basic
notation `⟪`x`⟫_`𝕜 := submodule.span 𝕜 {y | y = x}
variables {E : Type*} [add_comm_group E] [module ℝ E]
example (x y : E) (hy : y ∉ ⟪ x ⟫_ℝ) (hy' : y ≠ x) : y = 0 := sorry
```

#### Heather Macbeth (Dec 22 2020 at 23:33):

Thank you! What about the infix version, is there a way to get that working?

#### Heather Macbeth (Dec 22 2020 at 23:36):

Oh,

```
notation 𝕜`∙`x := submodule.span 𝕜 (set.insert x ∅)
```

seems to work. Maybe it's just a peculiarity of the `infix`

keyword that the other one didn't.

#### Heather Macbeth (Dec 22 2020 at 23:37):

At least, this works:

```
import linear_algebra.basic
import data.real.basic
notation 𝕜`∙`x := submodule.span 𝕜 (set.insert x ∅)
variables {E : Type*} [add_comm_group E] [module ℝ E]
example (x y : E) (hy : y ∉ (ℝ ∙ x)) (hy' : y ≠ x) : y = 0 := sorry
```

Is there something I can do with priorities that will let me ditch the parentheses in `(ℝ ∙ x)`

?

#### Adam Topaz (Dec 22 2020 at 23:39):

Maybe something like this?

```
import linear_algebra.basic
import data.real.basic
notation 𝕜`∙`:1000 x := submodule.span 𝕜 (set.insert x ∅)
variables {E : Type*} [add_comm_group E] [module ℝ E]
example (x y : E) (hy : y ∉ ℝ ∙ x) (hy' : y ≠ x) : y = 0 := sorry
```

#### Heather Macbeth (Dec 22 2020 at 23:40):

Awesome, thanks! One last question: is there a centralized list of unicode characters, so that I can find a dot character without any previous use in mathlib?

#### Adam Topaz (Dec 22 2020 at 23:45):

I think you have to look at the repo for the vscode extension.

#### Adam Topaz (Dec 22 2020 at 23:45):

(assuming you're using vscode :smile:)

#### Heather Macbeth (Dec 22 2020 at 23:46):

If I remember correctly, that lists all the unicode symbols that are taken. But how can I determine the complement? :)

#### Mario Carneiro (Dec 22 2020 at 23:55):

that list is not all taken characters, in fact most of them are free

#### Mario Carneiro (Dec 22 2020 at 23:55):

a better list would be `#print notation`

with all of mathlib imported

#### Mario Carneiro (Dec 22 2020 at 23:56):

alternatively, if you are looking specifically for unicode characters, you can just use the list in the repo and grep for uses of each of them in mathlib

#### Thomas Browning (Dec 23 2020 at 02:10):

Here's what we used for adjoin:

```
/--
Variation on `set.insert` to enable good notation for adjoining elements to fields.
Used to preferentially use `singleton` rather than `insert` when adjoining one element.
-/
--this definition of notation is courtesy of Kyle Miller on zulip
class insert {α : Type*} (s : set α) :=
(insert : α → set α)
@[priority 1000]
instance insert_empty {α : Type*} : insert (∅ : set α) :=
{ insert := λ x, @singleton _ _ set.has_singleton x }
@[priority 900]
instance insert_nonempty {α : Type*} (s : set α) : insert s :=
{ insert := λ x, set.insert x s }
notation K`⟮`:std.prec.max_plus l:(foldr `, ` (h t, insert.insert t h) ∅) `⟯` := adjoin K l
```

#### Thomas Browning (Dec 23 2020 at 02:10):

This made it so that K(x) was definitionally equal to `adjoin K {x}`

#### Thomas Browning (Dec 23 2020 at 02:11):

and it allowed for adjoining multiple elements at once

#### Heather Macbeth (Dec 23 2020 at 07:19):

Another way to do the original problem, adapting a trick from the code @Thomas Browning posted:

```
import linear_algebra.basic
import data.real.basic
notation 𝕜`∙`:1000 x := submodule.span 𝕜 (@singleton _ _ set.has_singleton x)
variables {E : Type*} [add_comm_group E] [module ℝ E]
example (x y : E) (hy : y ∉ (ℝ ∙ x)) (hy' : y ≠ x) : y = 0 := sorry
```

#### Adam Topaz (Jan 14 2021 at 04:23):

@Heather Macbeth did your new notation for the span of a vector get merged into mathlib yet?

#### Heather Macbeth (Jan 14 2021 at 04:24):

Yup, #5538.

#### Adam Topaz (Jan 14 2021 at 04:24):

Great! Thanks :)

Last updated: Aug 03 2023 at 10:10 UTC