Theorems · Theorem · commutative algebra

IsIntegral.inv_mem

∀ {R : Type u_1} {S : Type u_2} [inst : Field R] [inst_1 : DivisionRing S] [inst_2 : Algebra R S] {x : S}
  {A : Subalgebra R S}, IsIntegral R x → x ∈ A → x⁻¹ ∈ A

The inverse of an integral element in a subalgebra of a division ring over a field also lies in that subalgebra.

Defined in

Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Cited by

2 results in Mathlib

Foundations

Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldDivisionRingAlgebra