adjoin_simple_eq_adjoin_pow_expChar_of_isSeparable'

English

For a separable extension, F⟮a⟯ = F⟮a^q⟯ for any a and exponential char q.

Русский

Для разделяемого расширения F⟮a⟯ = F⟮a^q⟯ для любого a и экспоненциальной характерной q.

LaTeX

$$$\operatorname{adjoin} F\{a\} = \operatorname{adjoin} F\{a^q\}$$$

Lean4

/-- If `E / F` is a separable field extension of exponential characteristic `q`, then
`F⟮a⟯ = F⟮a ^ q⟯` for any `a : E`. -/
theorem adjoin_simple_eq_adjoin_pow_expChar_of_isSeparable' [Algebra.IsSeparable F E] (a : E) (q : ℕ) [ExpChar F q] :
    F⟮a⟯ = F⟮a ^ q⟯ :=
  pow_one q ▸ adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable' F E a q 1

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