English
A nonzero element in a domain that is integral over a field is a unit.
Русский
Не нулевой элемент в домене, интегральный над полем, является единицей.
LaTeX
$$$\\text{If } R \\text{ is a field and } S \\text{ a domain with } R\\text{-algebra, and } x \\text{ is integral over } R, x \\neq 0 \\Rightarrow x \\text{ is a unit in } S$$$
Lean4
/-- A nonzero element in a domain integral over a field is a unit. -/
theorem isUnit [Field R] [Ring S] [IsDomain S] [Algebra R S] {x : S} (int : IsIntegral R x) (h0 : x ≠ 0) : IsUnit x :=
have : FiniteDimensional R (adjoin R { x }) := ⟨(Submodule.fg_top _).mpr int.fg_adjoin_singleton⟩
(FiniteDimensional.isUnit R (K := adjoin R { x }) (x := ⟨x, subset_adjoin rfl⟩) <| mt Subtype.ext_iff.mp h0).map
(adjoin R { x }).val
