isAlgebraic_iff_isAlgebraic_val — Mathlib

English

TheIsAlgebraic property for a Subalgebra element is equivalent to that for its underlying value.

Русский

Свойство алгебраичности элемента подподмножества эквивалентно свойству для его базового значения.

LaTeX

$$$IsAlgebraic(R, x) \iff IsAlgebraic(R, x.1)$ for x ∈ Subalgebra.$$

Lean4

theorem isAlgebraic_iff_isAlgebraic_val {S : Subalgebra R A} {x : S} : IsAlgebraic R x ↔ IsAlgebraic R x.1 :=
  (isAlgebraic_algHom_iff S.val Subtype.val_injective).symm

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