isCancelMul_iff_forall_isRegular — Mathlib

English

In a nonempty ring-like structure, IsCancelMul is equivalent to every element being regular.

Русский

В структуре с умножением свойство IsCancelMul эквивалентно тому, что каждый элемент является регулярным.

LaTeX

$$$\text{IsCancelMul } R \iff \forall r:\, R, \text{IsRegular}(r)$$$

Lean4

@[to_additive]
theorem isCancelMul_iff_forall_isRegular [Mul R] : IsCancelMul R ↔ ∀ r : R, IsRegular r :=
  by
  rw [isCancelMul_iff, isLeftCancelMul_iff, isRightCancelMul_iff, ← forall_and]
  exact forall_congr' fun _ ↦ isRegular_iff.symm

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