isRightCancelMulZero_iff — Mathlib

English

IsRightCancelMulZero for R[X] is equivalent to IsRightCancelMulZero for R together with IsCancelAdd for R.

Русский

Правая отменяемость умножения на ноль в R[X] эквивалентна правой отменяемости в R и IsCancelAdd в R.

LaTeX

$$$\operatorname{IsRightCancelMulZero}(R[X]) \iff \operatorname{IsRightCancelMulZero}(R) \land \operatorname{IsCancelAdd}(R)$$$

Lean4

theorem isRightCancelMulZero_iff : IsRightCancelMulZero R[X] ↔ IsRightCancelMulZero R ∧ IsCancelAdd R := by
  rw [← MulOpposite.isLeftCancelMulZero_iff, (opRingEquiv R).isLeftCancelMulZero_iff, isLeftCancelMulZero_iff,
    MulOpposite.isLeftCancelMulZero_iff, MulOpposite.isCancelAdd_iff]

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