all — Mathlib

English

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

Русский

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

LaTeX

$$[IsLeftCancelMul R] ⇒ ∀ g:R, IsLeftRegular g$$

Lean4

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

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