isLeftRegular_of_non_zero_divisor
theorem isLeftRegular_of_non_zero_divisor :
∀ {α : Type u_1} [inst : NonUnitalNonAssocRing α] (k : α), (∀ (x : α), k * x = 0 → x = 0) → IsLeftRegular k := by
sorry
This theorem states that for any type `α` that forms a non-unital non-associative ring, multiplication on the left by any element `k` of `α` is injective, provided that `k` is not a zero divisor. In other words, if `k * x = 0` implies `x = 0` for all `x` in `α`, then `k` has the property that different inputs produce different outputs when multiplied by `k` from the left. This property of `k` is formalized by the predicate `IsLeftRegular`. The `NoZeroDivisors` typeclass is mentioned as it restricts all terms of `α` to have this property.
More concisely: For any non-unital non-associative ring type `α` without zero divisors, left multiplication by any non-zero element is an injection.
|
isRightRegular_of_non_zero_divisor
theorem isRightRegular_of_non_zero_divisor :
∀ {α : Type u_1} [inst : NonUnitalNonAssocRing α] (k : α), (∀ (x : α), x * k = 0 → x = 0) → IsRightRegular k := by
sorry
This theorem states that for any type `α` which has a structure of a non-unital non-associative ring, if we have an element `k` of `α` such that it is not a zero divisor (i.e., whenever an element `x` of `α` multiplied by `k` gives zero, `x` must be zero itself), then `k` is a right-regular element. In other words, multiplication on the right by `k` is an injective function. The typeclass `NoZeroDivisors` is used to restrict all terms of `α` to have this property.
More concisely: If `α` is a non-unital non-associative ring type with no zero divisors, then any non-zero divisor `k` in `α` is right-regular.
|