adjoin_eq_algebra_adjoin — Mathlib

English

If a finite Galois intermediate field K has its underlying subalgebra equal to Algebra.adjoin F S, then K equals adjoin F S.

Русский

Если конечное Галуа-подполе K имеет подалгебру, равную Algebra.adjoin F S, то K = adjoin F S.

LaTeX

$$K.toSubalgebra = Algebra.adjoin F S → K = adjoin F S$$

Lean4

theorem adjoin_eq_algebra_adjoin (inv_mem : ∀ x ∈ Algebra.adjoin F S, x⁻¹ ∈ Algebra.adjoin F S) :
    (adjoin F S).toSubalgebra = Algebra.adjoin F S :=
  le_antisymm
    (show adjoin F S ≤ { Algebra.adjoin F S with inv_mem' := inv_mem } from adjoin_le_iff.mpr Algebra.subset_adjoin)
    (algebra_adjoin_le_adjoin _ _)

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