adjoin_simple_map_algHom — Mathlib

English

If f is a k-algebra homomorphism, adjoin_k({f(x)}) = adjoin_k({x}) for any x ∈ K when IsGalois holds.

Русский

Если f — алгебра-гомоморфизм, то для любого x в K имеет место adjoin_k({f(x)}) = adjoin_k({x}) при выполнении условий IsGalois.

LaTeX

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

Lean4

@[simp]
theorem adjoin_simple_map_algHom [IsGalois k K] (f : K →ₐ[k] K) (x : K) : adjoin k {f x} = adjoin k { x } := by
  simpa only [Set.image_singleton] using adjoin_map f { x }

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