span_singleton_eq_bot simp?

Stream: maths

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Chris Hughes]

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]

Oh yes. Damn.

[Chris Hughes]

Hang on. Is there a loop?

[Mario Carneiro]

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]

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]

I just checked and I was wrong.

[Kevin Buzzard]

OK so I'll add simp to the two existing span_singleton_eq_bot lemmas and also add two new span_zero simp lemmas.