Theorems · Theorem · commutative algebra

isRegular_mul_and_mul_iff

∀ {R : Type u_1} [inst : Semigroup R] {a b : R}, IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b

Two elements a and b are regular if and only if both products a * b and b * a are regular.

Defined in

Mathlib.Algebra.Regular.Basic

Cited by

2 results in Mathlib

Foundations

Depth 9 from the axioms · uses propext, Quot.sound

Assumes

Semigroup