adjoin_val — Mathlib

English

The adjoin operation depends only on the set, not on its presentation; if s = s', then adjoin_k(s) = adjoin_k(s').

Русский

Операция приёма порождает (адьойн) зависит только от множества, не от его представления; если s = s', то adjoin_k(s) = adjoin_k(s').

LaTeX

$$$ s = s' \Rightarrow adjoin_k(s) = adjoin_k(s'). $$$

Lean4

@[simp]
theorem adjoin_val [IsGalois k K] (s : Set K) [Finite s] :
    (FiniteGaloisIntermediateField.adjoin k s) = normalClosure k (IntermediateField.adjoin k s) K :=
  rfl

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