isLeftCancelMulZero — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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