algebraMap_def — Mathlib

English

The algebra map from R[X] to A[X] equals the map obtained by applying algebraMap R A to the coefficients, i.e., algebraMap_{R[X]} A[X] = mapRingHom (algebraMap R A).

Русский

Алгебраическое отображение из R[X] в A[X] равняется отображению, полученному применением algebraMap R A к коэффициентам.

LaTeX

$$$\operatorname{algebraMap}_{R[X]} A[X] = \operatorname{mapRingHom}(\operatorname{algebraMap} R A).$$$

Lean4

@[simp]
theorem algebraMap_def : algebraMap R[X] A[X] = mapRingHom (algebraMap R A) :=
  rfl

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