instIsLeftCancelMulZeroOfIsCancelAdd

English

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

Русский

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

LaTeX

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

Lean4

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

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