iterateFrobeniusₛₗ_algebraMap

English

Let a ∈ K. Then iterating Frobenius on the bottom field and then embedding into L satisfies an equality with a^{p^n} in the same ambient field.

Русский

Пусть a ∈ K. Тогда применение Фробениуса к нижнему полю, после которого следует вложение в L, удовлетворяет равенству с a^{p^n} в L.

LaTeX

$$$\operatorname{iterateFrobenius}_{F,K,L,p,hn}(\operatorname{algebraMap}_{K,L}(a)) = \operatorname{algebraMap}_{K,L}(a^{p^n})$$$

Lean4

/-- Action of `iterateFrobeniusₛₗ` on the bottom field. -/
theorem iterateFrobeniusₛₗ_algebraMap {n : ℕ} (hn : exponent K L ≤ n) (a : K) :
    iterateFrobeniusₛₗ F K L p hn (algebraMap K L a) = a ^ p ^ n :=
  iterateFrobenius_algebraMap L p hn a

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