coe_frobeniusAlgEquivOfAlgebraic — Mathlib

English

For any algebraic K-L extension, the coercion of frobeniusAlgEquivOfAlgebraic K L equals x ↦ x^q.

Русский

Для любого алгебраического расширения K ⊂ L ковариантность frobeniusAlgEquivOfAlgebraic K L задаётся как x ↦ x^q.

LaTeX

$$AlgEquiv.instFunLike.coe (FiniteField.frobeniusAlgEquivOfAlgebraic K L) = (λ x, x^q)$$

Lean4

theorem coe_frobeniusAlgEquivOfAlgebraic [Algebra.IsAlgebraic K L] : ⇑(frobeniusAlgEquivOfAlgebraic K L) = (· ^ q) :=
  rfl

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