cancel_left — Mathlib

English

If f is an injective linear map, then for any g,g' : M1 → M2, f ∘ g = f ∘ g' implies g = g'.

Русский

Пусть f : M2 → M3 — линейное отображение и инъективно. Тогда для любых g,g' : M1 → M2 выполняется f ∘ g = f ∘ g' тогда и только тогда, когда g = g'.

LaTeX

$$$\\text{If } f: M_2 \\to M_3 \\text{ is injective, then for all } g,g': M_1 \\to M_2,\\ f \\circ g = f \\circ g' \\iff g = g'.}$$$

Lean4

@[simp]
theorem cancel_left (hf : Injective f) : f.comp g = f.comp g' ↔ g = g' :=
  hf.injective_linearMapComp_left.eq_iff

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