isLeftRegular_of_non_zero_divisor

English

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

Русский

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

LaTeX

$$$\forall x,y \in \alpha,\ kx = ky \Rightarrow x = y$$$

Lean4

/-- Left `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 isLeftRegular_of_non_zero_divisor [NonUnitalNonAssocRing α] (k : α) (h : ∀ x : α, k * x = 0 → x = 0) :
    IsLeftRegular k := by
  refine fun x y (h' : k * x = k * y) => sub_eq_zero.mp (h _ ?_)
  rw [mul_sub, sub_eq_zero, h']

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