English
For a fixed polynomial f over a commutative ring R, the AdjoinRoot f is the quotient of the polynomial ring R[X] by the ideal generated by f, and mk f is the canonical surjective map from R[X] to AdjoinRoot f sending X to the root of f.
Русский
Для кольца R и фиксированного многочлена f над R AdjoinRoot f является факторкольцом кольца R[X] по идеалу, порождаемому f; mk f — каноническое сюрьектирующее отображение R[X] в AdjoinRoot f, отправляющее X в корень f.
LaTeX
$$$AdjoinRoot(f) \\cong R[X]/(f)$$$
Lean4
/-- Ring homomorphism from `R[x]` to `AdjoinRoot f` sending `X` to the `root`. -/
def mk : R[X] →+* AdjoinRoot f :=
Ideal.Quotient.mk _
