instIsCancelMulZeroOfIsCancelAdd — Mathlib

English

If the base algebra R has cancellative addition and no zero divisors for multiplication, then the polynomial ring R[X] also has the cancellation property with respect to multiplication; in particular, for polynomials P, Q, R in R[X], if P ≠ 0 and P·Q = P·R, then Q = R.

Русский

Если базовая алгебра R обладает отменяемостью по сложению и не имеет нулевых делителей для умножения, то и полиномы над R, то есть R[X], обладают свойством отменяемости по умножению; в частности, для многочленов P, Q, R ∈ R[X], если P ≠ 0 и P·Q = P·R, то Q = R.

LaTeX

$$$P \neq 0 \land P Q = P R \Rightarrow Q = R$$$

Lean4

instance [IsCancelAdd R] [IsCancelMulZero R] : IsCancelMulZero R[X] where

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