adjoin_simple_map_algEquiv

Mathlib.FieldTheory.Galois.GaloisClosure

URI: https://scilib.ai/kg/mathlib#FiniteGaloisIntermediateField.adjoin_simple_map_algEquiv

← MathLib Explorer

English

If f is an IsGalois k K isomorphism, adjoin_k({f(x)}) = adjoin_k({x}) for any x ∈ K.

Русский

Если f — изоморфизм IsGalois k K, то adjoin_k({f(x)}) = adjoin_k({x}) для любого x.

LaTeX

$$$ adjoin_k(\{f x\}) = adjoin_k(\{x\}). $$$

Lean4

@[simp]
theorem adjoin_simple_map_algEquiv [IsGalois k K] (f : K ≃ₐ[k] K) (x : K) : adjoin k {f x} = adjoin k { x } :=
  adjoin_simple_map_algHom (f : K →ₐ[k] K) x

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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