coe_toAdjoin — Mathlib

English

The canonical linear map from the universal root object Minpoly.toAdjoin coincides with the universal lifting map along the generator of the adjoining algebra.

Русский

Каноническое отображение из Minpoly.toAdjoin совпадает с универсальным восходящим отображением по генератору присоединённой алгебры.

LaTeX

$$$\text{coe_toAdjoin}: = \text{liftHom}(\minpoly\;R\;x)\;\langle x, \text{self_mem_adjoin_singleton}\rangle$ (оператор-предположение).$$

Lean4

@[simp]
theorem coe_toAdjoin :
    ⇑(Minpoly.toAdjoin R x) =
      liftHom (minpoly R x) ⟨x, self_mem_adjoin_singleton R x⟩
        (by simp [← Subalgebra.coe_eq_zero, aeval_subalgebra_coe]) :=
  rfl

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