isLeftCancelMulZero_iff — Mathlib

English

Cancellation by left multiplication with zero is preserved under ring isomorphisms: IsLeftCancelMulZero A ↔ IsLeftCancelMulZero B.

Русский

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

LaTeX

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

Lean4

theorem isLeftCancelMulZero_iff (e : A ≃* B) : IsLeftCancelMulZero A ↔ IsLeftCancelMulZero B
    where
  mp _ := e.symm.injective.isLeftCancelMulZero _ (map_zero _) (map_mul _)
  mpr _ := e.injective.isLeftCancelMulZero _ (map_zero _) (map_mul _)

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