English
If x ∈ K is integral over A and the fractional ideal adjoinIntegral A⁰ x hx is a unit, then adjoinIntegral A⁰ x hx = 1.
Русский
Если x ∈ K цел по отношению к A, и дробный идеал adjoinIntegral A⁰ x hx является единицей, то adjoinIntegral A⁰ x hx = 1.
LaTeX
$$$$\\text{If } \\mathrm{adjoinIntegral}(A^\\circ, x, hx) \\text{ is a unit, then } \\mathrm{adjoinIntegral}(A^\\circ, x, hx) = 1.$$$$
Lean4
theorem adjoinIntegral_eq_one_of_isUnit [Algebra A K] [IsFractionRing A K] (x : K) (hx : IsIntegral A x)
(hI : IsUnit (adjoinIntegral A⁰ x hx)) : adjoinIntegral A⁰ x hx = 1 :=
by
set I := adjoinIntegral A⁰ x hx
have mul_self : IsIdempotentElem I := by
apply coeToSubmodule_injective
simp only [coe_mul, adjoinIntegral_coe, I]
rw [(Algebra.adjoin A { x }).isIdempotentElem_toSubmodule]
convert congr_arg (· * I⁻¹) mul_self <;> simp only [(mul_inv_cancel_iff_isUnit K).mpr hI, mul_assoc, mul_one]
