cancel_right — Mathlib

English

If f is surjective, then g1 ∘ f = g2 ∘ f implies g1 = g2 for MulHom; cancellation holds on the right.

Русский

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

LaTeX

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

Lean4

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

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