adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom

English

The inverse of the canonical isomorphism between F[a] and AdjoinRoot(minpoly F a) is the natural algebra hom AdjoinRoot(minpoly F a) →_F F[a], given by mapping the root to a.

Русский

Обратный к каноническому изоморфизму между F[a] и AdjoinRoot(minpoly F a) отображение есть естественный алгебра-гомоморфизм AdjoinRoot(minpoly F a) →_F F[a], посылка корня в a.

LaTeX

$$$(\\operatorname{adjoinSingletonEquivAdjoinRootMinpoly} F x)^{-1} = \\operatorname{AdjoinRoot.Minpoly.toAdjoin} F x$$$

Lean4

@[simp]
theorem adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom {R : Type*} [CommRing R] [Algebra F R] (x : R) :
    (adjoinSingletonEquivAdjoinRootMinpoly F x).symm = AdjoinRoot.Minpoly.toAdjoin F x :=
  rfl

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