isRegular_unop — Mathlib

English

Let R be a semigroup with multiplication. For any a in the opposite of R, the element a.unop ∈ R is regular in R iff a is regular in Rᵐᵒᵖ.

Русский

Пусть R — полугруппа с умножением. Пусть a ∈ Rᵐᵒᵖ. Тогда элемент a.unop ∈ R регулярен в R тогда и только тогда, когда сам a регулярен в Rᵐᵒᵖ.

LaTeX

$$$IsRegular(\mathrm{unop}(a)) \iff IsRegular(a)$$$

Lean4

@[to_additive (attr := simp)]
theorem isRegular_unop {a : Rᵐᵒᵖ} : IsRegular a.unop ↔ IsRegular a :=
  isRegular_op.symm

Похожие утверждения