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

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