coe_frobeniusAlgEquivOfAlgebraic_iterate

English

For algebraic K-L, the n-th iterate of frobeniusAlgEquivOfAlgebraic corresponds to raising to the power q^n.

Русский

Для алгебраического расширения K ⊂ L n-й итерации frobeniusAlgEquivOfAlgebraic соответствует возведению в степень q^n.

LaTeX

$$(frobeniusAlgEquivOfAlgebraic K L)^[n] = (· ^ (q^n))$$

Lean4

theorem coe_frobeniusAlgEquivOfAlgebraic_iterate [Algebra.IsAlgebraic K L] (n : ℕ) :
    (⇑(frobeniusAlgEquivOfAlgebraic K L))^[n] = (· ^ (Fintype.card K ^ n)) :=
  pow_iterate (Fintype.card K) n

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