inv_mem_adjoin — Mathlib

English

If x is integral over R and not zero, then x^{-1} lies in the subalgebra generated by x, i.e., in adjoin R {x}.

Русский

Если x интегральный над R и не нулевой, то x^{-1} принадлежит парам подалгебры, порожденной x.

LaTeX

$$$\\text{inv_mem_adjoin} : x^{-1} \\in \\mathrm{adjoin}\\ R\\{x\\}$$$

Lean4

theorem inv_mem_adjoin (int : IsIntegral R x) : x⁻¹ ∈ adjoin R { x } :=
  by
  obtain rfl | h0 := eq_or_ne x 0
  · rw [inv_zero]; exact Subalgebra.zero_mem _
  have : FiniteDimensional R (adjoin R { x }) := ⟨(Submodule.fg_top _).mpr int.fg_adjoin_singleton⟩
  obtain ⟨⟨y, hy⟩, h1⟩ :=
    FiniteDimensional.exists_mul_eq_one R (K := adjoin R { x }) (x := ⟨x, subset_adjoin rfl⟩) (mt Subtype.ext_iff.mp h0)
  rwa [← mul_left_cancel₀ h0 ((Subtype.ext_iff.mp h1).trans (mul_inv_cancel₀ h0).symm)]

Похожие утверждения