# Zulip Chat Archive

## Stream: maths

### Topic: span_singleton_eq_bot simp?

#### Kevin Buzzard (Jul 02 2020 at 12:07):

```
lemma span_singleton_eq_bot : span R ({x} : set M) = ⊥ ↔ x = 0 :=
span_eq_bot.trans $ by simp
```

There is one of these in `linear_algebra.basic`

(for modules) and another one in `ring_theory.ideals`

(for ideals). Should they be `simp`

lemmas? `simp`

can't solve `span R {0} = ⊥`

otherwise. Or should they not be `simp`

lemmas but I should add two simp lemmas `span_zero : span R {0} = ⊥`

?

#### Chris Hughes (Jul 02 2020 at 12:40):

They should be simp lemmas and so should `span R {0} = bot`

.

#### Mario Carneiro (Jul 02 2020 at 12:41):

I don't think they can both be simp lemmas because one shadows the other

#### Chris Hughes (Jul 02 2020 at 12:42):

That way `simp * at *`

will still simplify `span R {x}`

to `bot`

when there's a `h : span R{x} =bot `

even if `h`

gets simplified first.

#### Chris Hughes (Jul 02 2020 at 12:42):

Oh yes. Damn.

#### Chris Hughes (Jul 02 2020 at 12:43):

Hang on. Is there a loop?

#### Mario Carneiro (Jul 02 2020 at 12:43):

actually I take it back, you can prove `span R {0} = bot`

using `by simp`

but that doesn't mean that `span R {0} = x`

will simplify with only the rule `span R ({x} : set M) = ⊥ ↔ x = 0`

#### Kevin Buzzard (Jul 02 2020 at 13:00):

I had guessed that if I added `@[simp]`

to `span_singleton_eq_bot`

and also added `span_zero`

as a simp lemma then the linter would complain.

#### Kevin Buzzard (Jul 02 2020 at 13:01):

I just checked and I was wrong.

#### Kevin Buzzard (Jul 02 2020 at 13:08):

OK so I'll add simp to the two existing `span_singleton_eq_bot`

lemmas and also add two new `span_zero`

simp lemmas.

Last updated: May 18 2021 at 08:14 UTC