ofAdjoinRootEquiv — Mathlib

English

If S is R-algebra isomorphic to R[X]/(f), then S is IsAdjoinRoot S f; i.e., S is generated by adjoining a root of f.

Русский

Если S эквивалентна как R-алгебра к R[X]/(f), то S является IsAdjoinRoot S f; то есть S порождается присоединением корня f.

LaTeX

$$$ ofAdjoinRootEquiv (e) : IsAdjoinRoot S f $$$

Lean4

/-- If `S` is `R`-isomorphic to `R[X]/(f)`, then `S` is given by adjoining a root of `f`. -/
abbrev ofAdjoinRootEquiv (e : AdjoinRoot f ≃ₐ[R] S) : IsAdjoinRoot S f :=
  ofAlgEquiv (AdjoinRoot.isAdjoinRoot f) e

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