adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable'

English

For a separable extension E/F with exponential characteristic q, adjoining a set S yields the same field as adjoining the q-power of elements of S.

Русский

Для сепарабельного расширения E/F с характеристикой q единичная адъюнкция множества S равна адъюнкции q-ой степени элементов S.

LaTeX

$$$\operatorname{adjoin} F S = \operatorname{adjoin} F(\{x^q : x \in S\})$$$

Lean4

/-- If `E / F` is a separable field extension of exponential characteristic `q`, then
`F(S) = F(S ^ (q ^ n))` for any subset `S` of `E` and any natural number `n`. -/
theorem adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable' [Algebra.IsSeparable F E] (S : Set E) (q : ℕ) [ExpChar F q]
    (n : ℕ) : adjoin F S = adjoin F ((· ^ q ^ n) '' S) :=
  haveI := Algebra.isSeparable_tower_bot_of_isSeparable F (adjoin F S) E
  adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable F E S q n

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