mkOfAdjoinEqTop_root — Mathlib

English

If α generates S as an algebra and α is integral over R, then the root of minpoly R α in the constructed IsAdjoinRoot equals α.

Русский

Если α порождает S как алгебру и интегрален над R, то корень minpoly R α в построенной структуре IsAdjoinRoot равен α.

LaTeX

$$(IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂).root = α$$

Lean4

@[simp]
theorem mkOfAdjoinEqTop_root : (IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂).root = α := by
  simp [IsAdjoinRoot.mkOfAdjoinEqTop, IsAdjoinRoot.root]

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