toFunAlgHom — Mathlib

English

There is a canonical IsScalarTower structure on R, R[X], A[X], i.e., the actions are compatible in a natural way.

Русский

Существует каноническая структура IsScalarTower на R, R[X], A[X], то есть действия согласованы естественным образом.

LaTeX

$$IsScalarTower\$R\\, R[X] \\, A[X]\$$$

Lean4

/-- (Implementation detail).
The algebra homomorphism `A ⊗[R] R[X] →ₐ[R] A[X]`.
-/
def toFunAlgHom : A ⊗[R] R[X] →ₐ[R] A[X] :=
  algHomOfLinearMapTensorProduct (toFunLinear R A) (toFunLinear_mul_tmul_mul R A) (toFunLinear_one_tmul_one R A)

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