cancel_left — Mathlib

English

If f is injective and f ∘ g1 = f ∘ g2, then g1 = g2; conversely if g1 = g2 then f ∘ g1 = f ∘ g2.

Русский

Если f инъективен и f ∘ g1 = f ∘ g2, то g1 = g2; если g1 = g2, то f ∘ g1 = f ∘ g2.

LaTeX

$$$$ \text{If } f \text{ is injective},\ f \circ g_1 = f \circ g_2 \iff g_1 = g_2. $$$$

Lean4

theorem cancel_left {g₁ g₂ : A →ₐ[R] B} {f : B →ₐ[R] C} (hf : Function.Injective f) : f.comp g₁ = f.comp g₂ ↔ g₁ = g₂ :=
  ⟨fun h => AlgHom.ext <| fun _ ↦ hf.eq_iff.mp <| AlgHom.ext_iff.mp h _, fun h => h ▸ rfl⟩

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