English
If a scalar s acts on R without zero divisors (i.e., s has the NoZeroSmulDivisors property on R), then the same property holds for the polynomial ring R[X]: if s · f = 0 for f in R[X], then either s = 0 or f = 0.
Русский
Если скаляру s не являются нулевыми делителями на R (свойство NoZeroSmulDivisors на R), то то же свойство верно и для кольца многочленов R[X]: если s · f = 0 для f в R[X], то либо s = 0, либо f = 0.
LaTeX
$$$\forall s \in S, \forall f \in R[X],\, s \cdot f = 0 \Rightarrow (s = 0 \lor f = 0).$$$
Lean4
instance {S : Type*} [Zero S] [SMulZeroClass S R] [NoZeroSMulDivisors S R] : NoZeroSMulDivisors S R[X] where
eq_zero_or_eq_zero_of_smul_eq_zero
eq :=
(eq_zero_or_eq_zero_of_smul_eq_zero <| congr_arg toFinsupp eq).imp id
(congr_arg ofFinsupp)
-- to avoid a bug in the `ring` tactic
