inv_mem — Mathlib

English

The inverse of an integral element in a subalgebra lies in that subalgebra.

Русский

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

LaTeX

$$$x^{-1} \\in A$ given \\ IsIntegral R x\\text{ and } x \\in A$$$

Lean4

/-- The inverse of an integral element in a subalgebra of a division ring over a field
  also lies in that subalgebra. -/
theorem inv_mem (int : IsIntegral R x) (hx : x ∈ A) : x⁻¹ ∈ A :=
  adjoin_le (Set.singleton_subset_iff.mpr hx) int.inv_mem_adjoin

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