degree_minpolyGen

Mathlib.RingTheory.PowerBasis

URI: https://scilib.ai/kg/mathlib#PowerBasis.degree_minpolyGen

← MathLib Explorer

English

The degree of minpolyGen pb equals pb.dim.

Русский

Степень minpolyGen pb равна pb.dim.

LaTeX

$$degree( pb.minpolyGen ) = pb.dim$$

Lean4

theorem degree_minpolyGen [Nontrivial A] (pb : PowerBasis A S) : degree (minpolyGen pb) = pb.dim :=
  by
  unfold minpolyGen
  rw [degree_sub_eq_left_of_degree_lt] <;> rw [degree_X_pow]
  apply degree_sum_fin_lt

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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