Cancellative

Stream: Is there code for X?

[Xavier Xarles]

I am looking for something like this

import Mathlib.GroupTheory.Submonoid.Operations
import Mathlib.GroupTheory.Submonoid.Membership


/-- The submonoid of cancellative elements of a `Monoid` `R`. -/
def Cancellative (R : Type*) [Monoid R] : Submonoid R where
  carrier := { x | ∀ y z, y * x = z * x → y = z }
  one_mem' y z h := by rwa [mul_one,mul_one] at h
  mul_mem' hx₁ hx₂ y z h := by
    rw [← mul_assoc,←  mul_assoc] at h
    exact hx₁ y z (hx₂ (y * _) (z * _) h)

[Riccardo Brasca]

I don't think we have it. It's probably worth it to do it for semigroups.

[Riccardo Brasca]

And of course we want the various cancellative instances.

[Eric Wieser]

(Related to that final remark: #8428)

[Xavier Xarles]

By the various cancellative instances do you mean something like

import Mathlib.GroupTheory.Subsemigroup.Basic

def LeftCancellative (R : Type*) [Semigroup R] : Subsemigroup R where
  carrier := { x | ∀ y z, x * y = x * z → y = z }
  mul_mem' hx₁ hx₂ y z h := by
    rw [mul_assoc,mul_assoc] at h
    exact hx₂ y z (hx₁ (_ * y ) (_ * z) h)

def RightCancellative (R : Type*) [Semigroup R] : Subsemigroup R where
  carrier := { x | ∀ y z, y * x = z * x  → y = z }
  mul_mem' hx₁ hx₂ y z h := by
    rw [←mul_assoc,←mul_assoc] at h
    exact hx₁ y z (hx₂ (y * _) (z * _) h)

[Eric Wieser]

I think you can golf that by using docs#IsLeftRegular.mul