minpolyGen_eq

Mathlib.RingTheory.PowerBasis

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

← MathLib Explorer

English

pb.minpolyGen equals minpoly_A pb.gen.

Русский

pb.minpolyGen равен minpoly_A pb.gen.

LaTeX

$$pb.minpolyGen = minpoly A pb.gen$$

Lean4

@[simp]
theorem minpolyGen_eq (pb : PowerBasis A S) : pb.minpolyGen = minpoly A pb.gen :=
  by
  nontriviality A
  refine minpoly.unique' A _ pb.minpolyGen_monic pb.aeval_minpolyGen fun q hq => or_iff_not_imp_left.2 fun hn0 h0 => ?_
  exact (pb.dim_le_degree_of_root hn0 h0).not_gt (pb.degree_minpolyGen ▸ hq)

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

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

Разделы

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

Аффилиация

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