all — Mathlib

English

If right cancellation holds, then every element is right-regular.

Русский

Если существует правое отменение, тогда каждый элемент праворарегулярный.

LaTeX

$$[IsRightCancelMul R] ⇒ ∀ g:R, IsRightRegular g$$

Lean4

/-- If all multiplications cancel on the right then every element is right-regular. -/
@[to_additive /-- If all additions cancel on the right then every element is add-right-regular. -/
    ]
theorem all [Mul R] [IsRightCancelMul R] (g : R) : IsRightRegular g :=
  (isRightCancelMul_iff R).mp ‹_› _

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