orderOf_frobeniusAlgEquivOfAlgebraic

English

For finite L, the order of FrobeniusEquivOfAlgebraic equals finrank K L.

Русский

Для конечного L порядок frobeniusAlgEquivOfAlgebraic равен finrank K L.

LaTeX

$$orderOf (frobeniusAlgEquivOfAlgebraic K L) = Module.finrank K L$$

Lean4

theorem orderOf_frobeniusAlgEquivOfAlgebraic : orderOf (frobeniusAlgEquivOfAlgebraic K L) = Module.finrank K L := by
  simpa [orderOf_eq_iff Module.finrank_pos, DFunLike.ext_iff] using orderOf_frobeniusAlgHom K L

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