English
In a ring, NoZeroDivisors, IsLeftCancelMulZero, IsRightCancelMulZero, and IsCancelMulZero are all equivalent (a four-way equivalence).
Русский
В кольце свойства NoZeroDivisors, IsLeftCancelMulZero, IsRightCancelMulZero и IsCancelMulZero эквивалентны между собой (четырехсторонняя эквивалентность).
LaTeX
$$$\text{NoZeroDivisors}(R),\ \text{IsLeftCancelMulZero}(R),\ \text{IsRightCancelMulZero}(R),\ \text{IsCancelMulZero}(R)$ образуют эквивалентность; каждый из них эквивалент к остальным.$$
Lean4
/-- A (not necessarily unital or associative) ring with no zero divisors has cancellative
multiplication on both sides. Since either left or right cancellative multiplication implies
the absence of zero divisors, the four conditions are equivalent to each other. -/
theorem noZeroDivisors_tfae :
List.TFAE [NoZeroDivisors R, IsLeftCancelMulZero R, IsRightCancelMulZero R, IsCancelMulZero R] :=
by
simp_rw [isLeftCancelMulZero_iff, isRightCancelMulZero_iff, isCancelMulZero_iff_forall_isRegular,
isLeftRegular_iff_right_eq_zero_of_mul, isRightRegular_iff_left_eq_zero_of_mul, isRegular_iff_eq_zero_of_mul]
tfae_have 1 ↔ 2 := noZeroDivisors_iff_right_eq_zero_of_mul
tfae_have 1 ↔ 3 := noZeroDivisors_iff_left_eq_zero_of_mul
tfae_have 1 ↔ 4 := noZeroDivisors_iff_eq_zero_of_mul
tfae_finish
