coe_adjoinSingletonEquivAdjoinRootMinpoly_symm

English

The coe of the inverse of the singleton-adjoin equivalence equals the canonical toAdjoin map from AdjoinRoot(minpoly F x) to F[a].

Русский

Коэффициент обратного изоморфизма равен каноническому отображению toAdjoin из AdjoinRoot(minpoly F x) в F[a].

LaTeX

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

Lean4

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

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