English
If R is a ring, then the polynomial ring R[X] carries a natural ring structure, with addition and multiplication defined coefficientwise.
Русский
Если R — кольцо, то многочленное кольцо R[X] обладает естественной структурой кольца, сложение и умножение задаются покоэффициентно.
LaTeX
$$$R[X] \text{ is a ring whenever } R \text{ is a ring}$$$
Lean4
instance ring : Ring R[X] :=
fast_instance%Function.Injective.ring toFinsupp toFinsupp_injective (toFinsupp_zero (R := R)) toFinsupp_one
toFinsupp_add toFinsupp_mul toFinsupp_neg toFinsupp_sub (fun _ _ => toFinsupp_nsmul _ _)
(fun _ _ => toFinsupp_zsmul _ _) toFinsupp_pow (fun _ => rfl) fun _ => rfl
