adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable

English

If a is separable, adjoin of a equals adjoin of a to any q-power repeatedly.

Русский

Если a разделяемый, то F⟮a⟯ = F⟮a^{q^n}⟯ для любого n.

LaTeX

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

Lean4

/-- If `F` is a field of exponential characteristic `q`, `a : E` is separable over `F`, then
`F⟮a⟯ = F⟮a ^ q ^ n⟯` for any natural number `n`. -/
theorem adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable {a : E} (ha : IsSeparable F a) (q : ℕ) [ExpChar F q]
    (n : ℕ) : F⟮a⟯ = F⟮a ^ q ^ n⟯ :=
  by
  haveI := (isSeparable_adjoin_simple_iff_isSeparable F E).mpr ha
  simpa using adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable F E { a } q n

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