Left- and right-zero elements

IsLeftZero m (∀ a, m * a = m) and IsRightZero m (∀ a, a * m = m) are the semigroup-theoretic left and right zeros: the elements whose principal right, resp. left, ideal is {m}. They are companions of IsIdempotentElem — every one-sided zero is idempotent — and dual to each other under MulOpposite.

[UPSTREAM]: this would extend Mathlib/Algebra/Group/Idempotent.lean.

def IsLeftZero {M : Type u_1} [Mul M] (m : M) : Prop

m is a left zero: m * a = m for every a.

Equations

• IsLeftZero m = ∀ (a : M), m * a = m

def IsRightZero {M : Type u_1} [Mul M] (m : M) : Prop

m is a right zero: a * m = m for every a.

Equations

• IsRightZero m = ∀ (a : M), a * m = m

theorem isLeftZero_iff {M : Type u_1} [Mul M] {a : M} : IsLeftZero a ↔ ∀ (b : M), a * b = a

theorem isRightZero_iff {M : Type u_1} [Mul M] {a : M} : IsRightZero a ↔ ∀ (b : M), b * a = a

@[simp]

theorem isLeftZero_op {M : Type u_1} [Mul M] {a : M} : IsLeftZero (MulOpposite.op a) ↔ IsRightZero a

@[simp]

theorem isRightZero_op {M : Type u_1} [Mul M] {a : M} : IsRightZero (MulOpposite.op a) ↔ IsLeftZero a

theorem IsLeftZero.isIdempotentElem {M : Type u_1} [Mul M] {a : M} (h : IsLeftZero a) : IsIdempotentElem a

A left zero is idempotent.

theorem IsRightZero.isIdempotentElem {M : Type u_1} [Mul M] {a : M} (h : IsRightZero a) : IsIdempotentElem a

A right zero is idempotent.

theorem IsLeftZero.eq_of_isRightZero {M : Type u_1} [Mul M] {a b : M} (ha : IsLeftZero a) (hb : IsRightZero b) : a = b

A left zero and a right zero coincide; in particular a two-sided zero is unique.

@[simp]

theorem isLeftZero_zero {M : Type u_1} [MulZeroClass M] : IsLeftZero 0

@[simp]

theorem isRightZero_zero {M : Type u_1} [MulZeroClass M] : IsRightZero 0