instIsAlgebraicSubtypeMemSubalgebraAlgebraicClosure

English

Any element of the algebraicClosure subalgebra is algebraic over the base ring; the corresponding instance exists.

Русский

Любой элемент подалгебры algebraicClosure является алгебраичным над базовым кольцом; существует соответствующий инстанс.

LaTeX

$$$\\text{Algebra.IsAlgebraic}_R(\\mathrm{Subtype}\\,\\{x : S \\mid x \\in \\text{algebraicClosure}_R S}\\,)$$$

Lean4

instance [IsDomain R] : Algebra.IsAlgebraic R (Subalgebra.algebraicClosure R S) :=
  (Subalgebra.isAlgebraic_iff _).mp fun _ ↦ id

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