Add proofs for Ring and commutative semigroup

[Akshobhya1234]

In this PR add the folllowing proofs for Ring

• If x + x = x then x = 0
• x * (y - z) = x * y - x * z
• (y - z) * x = (y * x) - (z * x)

For commutative semigroup

• semimedial : Semimedial _∙_

[jamesmckinna]

I'm increasingly unsure about the value of the first lemma: is this not a simple consequence of cancellability, once it has been generalised to

• if x + y = y then x = 0?

The other two seem more useful, however.

[Akshobhya1234]

I'm increasingly unsure about the value of the first lemma: is this not a simple consequence of cancellability, once it has been generalised to

• if x + y = y then x = 0?

The other two seem more useful, however.

Hmm not sure. Isn't it x + y = x + z then y = z?. In this case y and z = 0 or y=x=z? The proof is If x+x=x then x = 0. I agree that we should not have duplicate proofs with different names.

[jamesmckinna]

Sorry I haven't got back to you... overwhelmed by other stuff.
I guess my point was, right-+-cancellation from x + y ≈ z + y would yield x ≈ z... and that x + y ≈ y, by left-identity, is equivalent to x + y ≈ z + y for z = 0#. And then your lemma follows by making the further identification y = x. So in that sense, it is 'just' (reducible to) a combination of cancellability and left-identity, and hence, maybe, not such an 'interesting' lemma? And if it is interesting enough to add to the library, then the generalisation to x + y ≈ y ⇒ x ≈ 0#, is surely the more 'useful' statement?

[Akshobhya1234]

Sorry I haven't got back to you... overwhelmed by other stuff. I guess my point was, right-+-cancellation from x + y ≈ z + y would yield x ≈ z... and that x + y ≈ y, by left-identity, is equivalent to x + y ≈ z + y for z = 0#. And then your lemma follows by making the further identification y = x. So in that sense, it is 'just' (reducible to) a combination of cancellability and left-identity, and hence, maybe, not such an 'interesting' lemma? And if it is interesting enough to add to the library, then the generalisation to x + y ≈ y ⇒ x ≈ 0#, is surely the more 'useful' statement?

Thanks @jamesmckinna I get your point. But x + y ≈ y ⇒ x ≈ 0# is same as left identity is unique +-identityˡ-unique. We have it when we export AbelianGroupProperties. But if you think we should not have this lemma I can remove it. :)

[jamesmckinna]

Thanks @Akshobhya1234

But x + y ≈ y ⇒ x ≈ 0# is same as left identity is unique +-identityˡ-unique. We have it when we export AbelianGroupProperties. But if you think we should not have this lemma I can remove it. :)

A very nice isolation of the essential property: so I would suggest then not to have your new lemma at all, but simply to instantiate that property at y = x at any point of use.

[Akshobhya1234]

Thanks @Akshobhya1234

But x + y ≈ y ⇒ x ≈ 0# is same as left identity is unique +-identityˡ-unique. We have it when we export AbelianGroupProperties. But if you think we should not have this lemma I can remove it. :)

A very nice isolation of the essential property: so I would suggest then not to have your new lemma at all, but simply to instantiate that property at y = x at any point of use.

Hmm I like to keep it. It comes under "Basic properties" of ring in many papers. Let's wait to see what @MatthewDaggitt has to say.

[MatthewDaggitt]

Hmm I like to keep it. It comes under "Basic properties" of ring in many papers. Let's wait to see what @MatthewDaggitt has to say.

Sorry for the late reply. I'm happy to keep the lemma, but I think @jamesmckinna is right in that it should definitely use the existing lemma to prove it, rather than reprove it from scratch!