Unit_Not_Zero_Divisor
Provedproofwikiringsunitszero-divisors
A unit of a ring is not a zero divisor.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Unit_Not_Zero_Divisor {R : Type _} [Ring R] [NoZeroDivisors R] (u : R) (hu : IsUnit u) (y : R) (h : u * y = 0) : y = 0 := by sorrySource