Results about IsRegular and MulOpposite

@[simp]

theorem isLeftRegular_op {R : Type u_1} [Mul R] {a : R} : IsLeftRegular (MulOpposite.op a) ↔ IsRightRegular a

@[simp]

theorem isAddLeftRegular_op {R : Type u_1} [Add R] {a : R} : IsAddLeftRegular (AddOpposite.op a) ↔ IsAddRightRegular a

@[simp]

theorem isRightRegular_op {R : Type u_1} [Mul R] {a : R} : IsRightRegular (MulOpposite.op a) ↔ IsLeftRegular a

@[simp]

theorem isAddRightRegular_op {R : Type u_1} [Add R] {a : R} : IsAddRightRegular (AddOpposite.op a) ↔ IsAddLeftRegular a

@[simp]

theorem isRegular_op {R : Type u_1} [Mul R] {a : R} : IsRegular (MulOpposite.op a) ↔ IsRegular a

@[simp]

theorem isAddRegular_op {R : Type u_1} [Add R] {a : R} : IsAddRegular (AddOpposite.op a) ↔ IsAddRegular a

theorem IsLeftRegular.op {R : Type u_1} [Mul R] {a : R} : IsRightRegular a → IsLeftRegular (MulOpposite.op a)

Alias of the reverse direction of isLeftRegular_op.

theorem IsAddLeftRegular.op {R : Type u_1} [Add R] {a : R} : IsAddRightRegular a → IsAddLeftRegular (AddOpposite.op a)

Alias of the reverse direction of isAddLeftRegular_op.

theorem IsRightRegular.op {R : Type u_1} [Mul R] {a : R} : IsLeftRegular a → IsRightRegular (MulOpposite.op a)

Alias of the reverse direction of isRightRegular_op.

theorem IsAddRightRegular.op {R : Type u_1} [Add R] {a : R} : IsAddLeftRegular a → IsAddRightRegular (AddOpposite.op a)

Alias of the reverse direction of isAddRightRegular_op.

theorem IsRegular.op {R : Type u_1} [Mul R] {a : R} : IsRegular a → IsRegular (MulOpposite.op a)

Alias of the reverse direction of isRegular_op.

theorem IsAddRegular.op {R : Type u_1} [Add R] {a : R} : IsAddRegular a → IsAddRegular (AddOpposite.op a)

Alias of the reverse direction of isAddRegular_op.

@[simp]

theorem isLeftRegular_unop {R : Type u_1} [Mul R] {a : Rᵐᵒᵖ} : IsLeftRegular (MulOpposite.unop a) ↔ IsRightRegular a

@[simp]

theorem isAddLeftRegular_unop {R : Type u_1} [Add R] {a : Rᵃᵒᵖ} : IsAddLeftRegular (AddOpposite.unop a) ↔ IsAddRightRegular a

@[simp]

theorem isRightRegular_unop {R : Type u_1} [Mul R] {a : Rᵐᵒᵖ} : IsRightRegular (MulOpposite.unop a) ↔ IsLeftRegular a

@[simp]

theorem isAddRightRegular_unop {R : Type u_1} [Add R] {a : Rᵃᵒᵖ} : IsAddRightRegular (AddOpposite.unop a) ↔ IsAddLeftRegular a

@[simp]

theorem isRegular_unop {R : Type u_1} [Mul R] {a : Rᵐᵒᵖ} : IsRegular (MulOpposite.unop a) ↔ IsRegular a

@[simp]

theorem isAddRegular_unop {R : Type u_1} [Add R] {a : Rᵃᵒᵖ} : IsAddRegular (AddOpposite.unop a) ↔ IsAddRegular a

theorem IsLeftRegular.unop {R : Type u_1} [Mul R] {a : Rᵐᵒᵖ} : IsRightRegular a → IsLeftRegular (MulOpposite.unop a)

Alias of the reverse direction of isLeftRegular_unop.

theorem IsAddLeftRegular.unop {R : Type u_1} [Add R] {a : Rᵃᵒᵖ} : IsAddRightRegular a → IsAddLeftRegular (AddOpposite.unop a)

Alias of the reverse direction of isAddLeftRegular_unop.

theorem IsRightRegular.unop {R : Type u_1} [Mul R] {a : Rᵐᵒᵖ} : IsLeftRegular a → IsRightRegular (MulOpposite.unop a)

Alias of the reverse direction of isRightRegular_unop.

theorem IsAddRightRegular.unop {R : Type u_1} [Add R] {a : Rᵃᵒᵖ} : IsAddLeftRegular a → IsAddRightRegular (AddOpposite.unop a)

Alias of the reverse direction of isAddRightRegular_unop.

theorem IsRegular.unop {R : Type u_1} [Mul R] {a : Rᵐᵒᵖ} : IsRegular a → IsRegular (MulOpposite.unop a)

Alias of the reverse direction of isRegular_unop.

theorem IsAddRegular.unop {R : Type u_1} [Add R] {a : Rᵃᵒᵖ} : IsAddRegular a → IsAddRegular (AddOpposite.unop a)

Alias of the reverse direction of isAddRegular_unop.