isAlgebraic_iff

Mathlib.FieldTheory.IntermediateField.Algebraic

URI: https://scilib.ai/kg/mathlib#IntermediateField.isAlgebraic_iff

English

For S ∈ IntermediateField, IsAlgebraic K x is equivalent to IsAlgebraic K x.val for x in S.

Русский

Для x ∈ S: IsAlgebraic K x эквивалентно IsAlgebraic K x.

LaTeX

$$$ IsAlgebraic\_K\; x \;\iff\; IsAlgebraic\_K\; x^{\text{val}} $$$

Lean4

theorem isAlgebraic_iff {x : S} : IsAlgebraic K x ↔ IsAlgebraic K (x : L) :=
  (isAlgebraic_algebraMap_iff (algebraMap S L).injective).symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru