card_of_separable — Mathlib

English

For a separable polynomial p, the cardinality of its Galois group equals the degree of its splitting field over F; i.e., |p.Gal| = finrank_F p.SplittingField.

Русский

Для разделимого многочлена p кардинальность его Галуа-группы равна размерности его разворачивающего поля над F; то есть |p.Gal| = finrank_F p.SplittingField.

LaTeX

$$$|p.Gal| = \\operatorname{finrank}_F(p.SplittingField)$$$

Lean4

/-- For a separable polynomial, its Galois group has cardinality
equal to the dimension of its splitting field over `F`. -/
theorem card_of_separable (hp : p.Separable) : Nat.card p.Gal = finrank F p.SplittingField :=
  haveI : IsGalois F p.SplittingField := IsGalois.of_separable_splitting_field hp
  IsGalois.card_aut_eq_finrank F p.SplittingField

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