isRightCancelMulZero_iff — Mathlib

English

Cancellation by right multiplication with zero is preserved under ring isomorphisms: IsRightCancelMulZero A ↔ IsRightCancelMulZero B.

Русский

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

LaTeX

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

Lean4

theorem isRightCancelMulZero_iff (e : A ≃* B) : IsRightCancelMulZero A ↔ IsRightCancelMulZero B
    where
  mp _ := e.symm.injective.isRightCancelMulZero _ (map_zero _) (map_mul _)
  mpr _ := e.injective.isRightCancelMulZero _ (map_zero _) (map_mul _)

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