cancel_left — Mathlib

English

Duplicate formulation: surjective f implies right-cancellation for MonoidHom.

Русский

Дубликат формулировки: сюръективное f обеспечивает правую отмену для MonoidHom.

LaTeX

$$$\\text{Surjective}(f) \\Rightarrow (g_1 \\circ f = g_2 \\circ f \\iff g_1 = g_2)$$$

Lean4

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

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