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

Yup, #5538.

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

Great! Thanks :)

Last updated: Dec 20 2023 at 11:08 UTC