isCancelMulZero_iff — Mathlib

English

Cancellation by both sides with zero is preserved under ring isomorphisms: IsCancelMulZero A ↔ IsCancelMulZero B.

Русский

Сохранение отменяемости при умножении на ноль слева и справа сохраняется при изоморфизмах колец.

LaTeX

$$$ (e : A \simeq* B) : IsCancelMulZero A \iff IsCancelMulZero B $$$

Lean4

theorem isCancelMulZero_iff (e : A ≃* B) : IsCancelMulZero A ↔ IsCancelMulZero B
    where
  mp _ := e.symm.injective.isCancelMulZero _ (map_zero _) (map_mul _)
  mpr _ := e.injective.isCancelMulZero _ (map_zero _) (map_mul _)

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