isCancelMulZero_iff — Mathlib

English

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

Русский

IsCancelMulZero для R[X] эквивалентно IsCancelMulZero для R и IsCancelAdd для R.

LaTeX

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

Lean4

protected theorem isCancelMulZero_iff : IsCancelMulZero R[X] ↔ IsCancelMulZero R ∧ IsCancelAdd R :=
  by
  simp_rw [isCancelMulZero_iff, isLeftCancelMulZero_iff, isRightCancelMulZero_iff]
  rw [and_and_and_comm, and_self]

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