mem_adjoin_simple_self

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

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

English

For α ∈ E, we have α ∈ F⟮α⟯, i.e., α lies in the simple extension generated by α over F.

Русский

Для α ∈ E верно α ∈ F⟮α⟯, т.е. α принадлежит простому расширению F(α).

LaTeX

$$$\\\\alpha \\\\in F\\\\langle \\\\alpha \rangle$$$

Lean4

theorem mem_adjoin_simple_self : α ∈ F⟮α⟯ :=
  subset_adjoin F { α } (Set.mem_singleton α)

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

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

Разделы

Аффилиация

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