isRightCancelMulZero — Mathlib

English

If f: M0 → M0' is injective and preserves multiplication with f 0 = 0, and M0' has IsRightCancelMulZero, then M0 also has IsRightCancelMulZero.

Русский

Если f: M0 → M0' инъективна и сохраняет умножение, и f 0 = 0, то правое отменяющее свойство скачет к M0.

LaTeX

$$$\\text{IsRightCancelMulZero } M_0' \\Rightarrow \\text{IsRightCancelMulZero } M_0$$$

Lean4

protected theorem isRightCancelMulZero [IsRightCancelMulZero M₀'] : IsRightCancelMulZero M₀ where
  mul_right_cancel_of_ne_zero Hne _ _
    He := by
    have := congr_arg f He
    rw [mul, mul] at this
    exact hf (mul_right_cancel₀ (fun Hfa => Hne <| hf <| by rw [Hfa, zero]) this)

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