instIsDomainOfIsCancelAdd — Mathlib

English

IsCancelMulZero transfers to MvPolynomial: product zero implies one factor zero, under suitable conditions.

Русский

Свободно переносится в MvPolynomial свойство Cancel MulZero: произведение равно нулю, значит один множитель равен нулю, при определённых условиях.

LaTeX

$$$ IsCancelMulZero( MvPolynomial\; σ\; R ) $$$

Lean4

/-- The multivariate polynomial ring over an integral domain is an integral domain. -/
instance [CommSemiring R] [IsCancelAdd R] [IsDomain R] : IsDomain (MvPolynomial σ R) where

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