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