finInsepDegree_eq_pow — Mathlib

English

For any natural q and finite-dimensional E over F, there exists n with finInsepDegree F E = q^n.

Русский

Для любого натурального q и конечномодульного E/ F существует n, такое что finInsepDegree F E = q^n.

LaTeX

$$$\exists n,\; \operatorname{finInsepDegree} F E = q^{n}$$$

Lean4

theorem finInsepDegree_eq_pow (q : ℕ) [ExpChar F q] [FiniteDimensional F E] : ∃ n, finInsepDegree F E = q ^ n :=
  IsPurelyInseparable.finrank_eq_pow ..

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