isAlgebraic_adjoin_iff — Mathlib

English

For any x in S, the element x is algebraic over the subalgebra adjoin_F_s inside S if and only if x is algebraic over Algebra.adjoin_F_s inside S; i.e., IsAlgebraic(adjoin F s) x is equivalent to IsAlgebraic(Algebra.adjoin F s) x.

Русский

Для любого x ∈ S свойство алгебраичности над подалгеброй adjoin_F_s внутри S эквивалентно алгебраичности над Algebra.adjoin_F_s внутри S; IsAlgebraic(adjoin F s) x эквивалентно IsAlgebraic(Algebra.adjoin F s) x.

LaTeX

$$$\\\\mathrm{IsAlgebraic}(\\\\operatorname{adjoin}_F s)\,x \\\\iff \\\\mathrm{IsAlgebraic}(\\\\operatorname{Algebra.adjoin}_F s)\,x$$$

Lean4

theorem isAlgebraic_adjoin_iff {x : S} : IsAlgebraic (adjoin F s) x ↔ IsAlgebraic (Algebra.adjoin F s) x :=
  (IsAlgebraic.isAlgebraic_iff ..).symm

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