bijective_frobeniusAlgHom_pow — Mathlib

English

For finite L over K, the map n ↦ frobeniusAlgHom^n is bijective on Fin (finrank K L).

Русский

Для конечного расширения L/K отображение n ↦ frobeniusAlgHom^n является биективным на Fin (finrank_K L).

LaTeX

$$Function.Bijective (fun n : Fin (Module.finrank K L) => frobeniusAlgHom K L ^ n.1)$$

Lean4

theorem bijective_frobeniusAlgHom_pow :
    Function.Bijective fun n : Fin (Module.finrank K L) ↦ frobeniusAlgHom K L ^ n.1 :=
  let e :=
    (finCongr <| orderOf_frobeniusAlgHom K L).symm.trans <|
      finEquivPowers (orderOf_pos_iff.mp <| orderOf_frobeniusAlgHom K L ▸ Module.finrank_pos)
  (Subtype.val_injective.comp e.injective).bijective_of_nat_card_le ((card_algHom_le_finrank K L L).trans_eq <| by simp)

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