English
If R is a commutative semiring and A is an R-algebra, then A[X] carries a natural R-algebra structure extending the given R-algebra on A.
Русский
Если R — коммутативная полускольная, а A — R-алгебра, то A[X] естественным образом имеет структуру R-алгебры, расширяющую заданную на A.
LaTeX
$$$\mathrm{Algebra}\; R\; A[X]$$$
Lean4
/-- Note that this instance also provides `Algebra R R[X]`. -/
instance algebraOfAlgebra : Algebra R A[X]
where
smul_def' r
p :=
toFinsupp_injective <| by
dsimp only [RingHom.toFun_eq_coe, RingHom.comp_apply]
rw [toFinsupp_smul, toFinsupp_mul, toFinsupp_C]
exact Algebra.smul_def' _ _
commutes' r
p :=
toFinsupp_injective <| by
dsimp only [RingHom.toFun_eq_coe, RingHom.comp_apply]
simp_rw [toFinsupp_mul, toFinsupp_C]
convert Algebra.commutes' r p.toFinsupp
algebraMap := C.comp (algebraMap R A)
