Unit_of_Integral_Domain_divides_all_Elements
Proveddivisibilityintegral-domainsproofwikiunits
In an integral domain, every unit divides every element.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Unit_of_Integral_Domain_divides_all_Elements {D : Type _} [CommRing D] [IsDomain D] (u : D) (hu : IsUnit u) (x : D) : u ∣ x := by sorrySource