cancel_right — Mathlib

English

If f is surjective, then g1 ∘ f = g2 ∘ f implies g1 = g2 for MonoidHom; right-cancellation property.

Русский

Если f сюръективен, то g1 ∘ f = g2 ∘ f ⇒ g1 = g2 для MonoidHom; правая отмена.

LaTeX

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

Lean4

@[to_additive]
theorem cancel_right [MulOne M] [MulOne N] [MulOne P] {g₁ g₂ : N →* P} {f : M →* N} (hf : Function.Surjective f) :
    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => MonoidHom.ext <| hf.forall.2 (DFunLike.ext_iff.1 h), fun h => h ▸ rfl⟩

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