adjoinRootAlgEquiv — Mathlib

English

There exists an algebra isomorphism between AdjoinRoot f and S over R, i.e., AdjoinRoot f ≃ₐ[R] S.

Русский

Существует алгебраическое изоморождение между AdjoinRoot f и S над R: AdjoinRoot f ≃ₐ[R] S.

LaTeX

$$$\operatorname{AdjoinRoot} f \cong_R S$$$

Lean4

/-- Algebra isomorphism with `R[X]/(f)`. -/
def adjoinRootAlgEquiv : AdjoinRoot f ≃ₐ[R] S :=
  (Ideal.quotientEquivAlgOfEq R h.ker_map.symm).trans <| Ideal.quotientKerAlgEquivOfSurjective h.map_surjective

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