isUnit_iff_mem_nonZeroDivisors_of_finite

English

In a finite ring, an element is a unit if and only if it is not a zero divisor.

Русский

В конечном кольце элемент является единицей тогда и только тогда, когда он не является нулевым делителем.

LaTeX

$$$a \in R^{\times} \iff a \in \operatorname{NZD}(R)$$$

Lean4

/-- In a finite ring, an element is a unit iff it is a non-zero-divisor. -/
theorem isUnit_iff_mem_nonZeroDivisors_of_finite [Finite R] : IsUnit a ↔ a ∈ nonZeroDivisors R := by
  rw [← isRegular_iff_mem_nonZeroDivisors, isRegular_iff_isUnit_of_finite]

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