cancel_left — Mathlib

English

If g is injective, then g ∘ f1 = g ∘ f2 implies f1 = f2 for MulHom; left-cancellation holds.

Русский

Если g инъективен, то g ∘ f1 = g ∘ f2 ⇒ f1 = f2 для MulHom; левая отмена.

LaTeX

$$$\\text{Injective}(g) \\Rightarrow (g\\circ f_1 = g\\circ f_2 \\iff f_1 = f_2)$$$

Lean4

@[to_additive]
theorem cancel_left [Mul M] [Mul N] [Mul P] {g : N →ₙ* P} {f₁ f₂ : M →ₙ* N} (hg : Function.Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => MulHom.ext fun x => hg <| by rw [← MulHom.comp_apply, h, MulHom.comp_apply], fun h => h ▸ rfl⟩

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