English
The canonical coe (coe) agrees with the liftHom construction for the toAdjoin map.
Русский
Каноническое включение согласуется с конструктором liftHom для отображения toAdjoin.
LaTeX
$$coe_toAdjoin: = ∙$$
Lean4
/-- If `L` is a field extension of `F` and `f` is a polynomial over `F` then the set
of maps from `F[x]/(f)` into `L` is in bijection with the set of roots of `f` in `L`. -/
def equiv (f : F[X]) (hf : f ≠ 0) : (AdjoinRoot f →ₐ[F] L) ≃ { x // x ∈ f.aroots L } :=
(powerBasis hf).liftEquiv'.trans
((Equiv.refl _).subtypeEquiv fun x =>
by
rw [powerBasis_gen, minpoly_root hf, aroots_mul, aroots_C, add_zero, Equiv.refl_apply]
exact (monic_mul_leadingCoeff_inv hf).ne_zero)
