adjoin_map — Mathlib

English

For an algebra automorphism f of K over k and a finite set s, adjoin_k(f''s) = adjoin_k(s).

Русский

Для автогеноморфизма f_K/k и конечного множества s имеет место adjoin_k(f''s) = adjoin_k(s).

LaTeX

$$$ adjoin_k(f''s) = adjoin_k(s). $$$

Lean4

@[simp]
theorem adjoin_map [IsGalois k K] (f : K →ₐ[k] K) (s : Set K) [Finite s] : adjoin k (f '' s) = adjoin k s :=
  by
  apply val_injective; dsimp [adjoin_val]
  rw [← IntermediateField.adjoin_map, IntermediateField.normalClosure_map_eq]

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