cancel_right — Mathlib

English

If f is surjective, then g1 ∘ f = g2 ∘ f implies g1 = g2 for order monoid with zero homomorphisms.

Русский

Если f сюръективен, то g1 ∘ f = g2 ∘ f приводит к g1 = g2 для OrderMonoidWithZeroHom.

LaTeX

$$$(g_1 \circ f) = (g_2 \circ f) \Rightarrow g_1 = g_2$ (при $\mathrm{Surjective}(f)$)$$

Lean4

@[simp]
theorem cancel_right {g₁ g₂ : β →*₀o γ} {f : α →*₀o β} (hf : Function.Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, fun _ => by congr⟩

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