range_val

Mathlib.FieldTheory.IntermediateField.Basic

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

English

The image of the embedding S.val equals S.toSubalgebra, i.e., the range of S.val is exactly the subalgebra corresponding to S inside L.

Русский

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

LaTeX

$$$ S.val.range = S.toSubalgebra $$$

Lean4

theorem range_val : S.val.range = S.toSubalgebra :=
  S.toSubalgebra.range_val

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

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

Разделы

Аффилиация

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