instIsRightCancelMulZeroOfIsCancelAdd

English

If R has IsCancelAdd and IsRightCancelMulZero, then R[X] also has these properties.

Русский

Если R удовлетворяет IsCancelAdd и IsRightCancelMulZero, то R[X] также удовлетворяет этим свойствам.

LaTeX

$$IsRightCancelMulZero(R) ⇒ IsRightCancelMulZero(R[X])$$

Lean4

instance [IsCancelAdd R] [IsRightCancelMulZero R] : IsRightCancelMulZero R[X] :=
  (toFinsuppIso R).injective.isRightCancelMulZero _ (map_zero _) (map_mul _)

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