English
If an element a is IsSMulRegular on R, then it is IsSMulRegular on the polynomial ring R[X].
Русский
Если элемент a обладает свойством IsSMulRegular на R, то он обладает тем же свойством на кольце полиномов R[X].
LaTeX
$$$\\operatorname{IsSMulRegular}(R, a) \\Rightarrow \\operatorname{IsSMulRegular}(R[X], a)$$$
Lean4
theorem _root_.IsSMulRegular.polynomial {S : Type*} [SMulZeroClass S R] {a : S} (ha : IsSMulRegular R a) :
IsSMulRegular R[X] a
| ⟨_x⟩, ⟨_y⟩, h => congr_arg _ <| ha.finsupp (Polynomial.ofFinsupp.inj h)