inv_mem — Mathlib

English

If an integral x has its inverse in a subalgebra, then x itself lies in the subalgebra.

Русский

Если интегральный x имеет обратный элемент в подалгебре, то x принадлежит этой подалгебре.

LaTeX

$$$\\text{If } int: IsIntegral R x \\text{ and } inv\\_mem: x^{-1} \\in A, \\text{ then } x \\in A$$$

Lean4

/-- An integral subalgebra of a division ring over a field is closed under inverses. -/
theorem inv_mem [Algebra.IsIntegral R A] (hx : x ∈ A) : x⁻¹ ∈ A :=
  ((isIntegral_algHom_iff A.val Subtype.val_injective).mpr <| Algebra.IsIntegral.isIntegral (⟨x, hx⟩ : A)).inv_mem hx

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