isRightRegular_iff_left_eq_zero_of_mul

English

IsRightRegular r iff ∀ x, x r = 0 ⇒ x = 0.

Русский

Правое регулярное: IsRightRegular r эквивалентно ∀ x, x r = 0 ⇒ x = 0.

LaTeX

$$$\text{IsRightRegular}(r) \iff \forall x,\ x\,r = 0 \Rightarrow x = 0$$$

Lean4

theorem isRightRegular_iff_left_eq_zero_of_mul : IsRightRegular r ↔ ∀ x, x * r = 0 → x = 0
    where
  mp h r' eq := h (by simp_rw [eq, zero_mul])
  mpr h r₁ r₂ eq := sub_eq_zero.mp <| h _ <| by simp_rw [sub_mul, eq, sub_self]

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