fieldRange_val

Mathlib.FieldTheory.IntermediateField.Basic

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

English

The fieldRange of the embedding S.val is exactly S; i.e., the image of the embedding equals the subfield S inside L.

Русский

Образ поля вложения S.val точно равен S; образ вложения совпадает со подполем S внутри L.

LaTeX

$$$ S.val.fieldRange = S $$$

Lean4

@[simp]
theorem fieldRange_val : S.val.fieldRange = S :=
  SetLike.ext' Subtype.range_val

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

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

Разделы

Аффилиация

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