Regular elements

We introduce left-regular, right-regular and regular elements, along with their to_additive analogues add-left-regular, add-right-regular and add-regular elements.

For monoids where every element is regular, see IsCancelMul and nearby typeclasses.

def IsLeftRegular {R : Type u_1} [Mul R] (c : R) : Prop

A left-regular element is an element c such that multiplication on the left by c is injective.

Equations

• IsLeftRegular c = Function.Injective fun (x : R) => c * x

def IsAddLeftRegular {R : Type u_1} [Add R] (c : R) : Prop

An add-left-regular element is an element c such that addition on the left by c is injective.

Equations

• IsAddLeftRegular c = Function.Injective fun (x : R) => c + x

def IsRightRegular {R : Type u_1} [Mul R] (c : R) : Prop

A right-regular element is an element c such that multiplication on the right by c is injective.

Equations

• IsRightRegular c = Function.Injective fun (x : R) => x * c

def IsAddRightRegular {R : Type u_1} [Add R] (c : R) : Prop

An add-right-regular element is an element c such that addition on the right by c is injective.

Equations

• IsAddRightRegular c = Function.Injective fun (x : R) => x + c

structure IsAddRegular {R : Type u_2} [Add R] (c : R) : Prop

An add-regular element is an element c such that addition by c both on the left and on the right is injective.

• left : IsAddLeftRegular c

  An add-regular element c is left-regular

• right : IsAddRightRegular c

  An add-regular element c is right-regular

structure IsRegular {R : Type u_1} [Mul R] (c : R) : Prop

A regular element is an element c such that multiplication by c both on the left and on the right is injective.

• left : IsLeftRegular c

  A regular element c is left-regular

• right : IsRightRegular c

  A regular element c is right-regular

theorem isRegular_iff {R : Type u_1} [Mul R] {c : R} : IsRegular c ↔ IsLeftRegular c ∧ IsRightRegular c

theorem isAddRegular_iff {R : Type u_1} [Add R] {c : R} : IsAddRegular c ↔ IsAddLeftRegular c ∧ IsAddRightRegular c