isIntegral — Mathlib

English

The F-vector space dimension of FixedPoints.subfield G F, viewed as a vector space over F, is at most the order of G. Equivalently, the module rank of FixedPoints.subfield G F over F is ≤ |G|.

Русский

Размерность пространства над F, полученного как FixedPoints.subfield G F, не превосходит порядка группы G.

LaTeX

$$$\\operatorname{rank}_F(\\operatorname{FixedPoints.subfield } G F) \\le |G|$$$

Lean4

theorem isIntegral [Finite G] (x : F) : IsIntegral (FixedPoints.subfield G F) x := by cases nonempty_fintype G;
  exact ⟨minpoly G F x, minpoly.monic G F x, minpoly.eval₂ G F x⟩

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