isRightRegular_of_non_zero_divisor

English

If k is not a right zero divisor, then right multiplication by k is injective.

Русский

Если k не правых нулевых делителей, то умножение справа на k инъективно.

LaTeX

$$$\forall x,y \in \alpha,\ xk = yk \Rightarrow x = y$$$

Lean4

/-- Right `Mul` by a `k : α` over `[Ring α]` is injective, if `k` is not a zero divisor.
The typeclass that restricts all terms of `α` to have this property is `NoZeroDivisors`. -/
theorem isRightRegular_of_non_zero_divisor [NonUnitalNonAssocRing α] (k : α) (h : ∀ x : α, x * k = 0 → x = 0) :
    IsRightRegular k := by
  refine fun x y (h' : x * k = y * k) => sub_eq_zero.mp (h _ ?_)
  rw [sub_mul, sub_eq_zero, h']

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