cardPowDegree_nonzero

Mathlib.Algebra.Polynomial.Degree.CardPowDegree

URI: https://scilib.ai/kg/mathlib#Polynomial.cardPowDegree_nonzero

English

If p ∈ Fq[X] is nonzero, then cardPowDegree p = (card Fq) ^ natDegree(p).

Русский

Если p ∈ F_q[X] ненулевой, то cardPowDegree p = (карта F_q)^{natDegree(p)}.

LaTeX

$$$\operatorname{cardPowDegree}(p) = (|F_q|)^{\operatorname{natDegree}(p)}$$$

Lean4

@[simp]
theorem cardPowDegree_nonzero (p : Fq[X]) (hp : p ≠ 0) : cardPowDegree p = (Fintype.card Fq : ℤ) ^ p.natDegree :=
  if_neg hp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru