cancel_right — Mathlib

English

If f: α →*o β is surjective, then right-cancellation holds for addition-analogs: g1.comp f = g2.comp f iff g1 = g2.

Русский

Если f является сюръективным гомоморфизмом, то правое аннулирование выполняется и для аддитивного аналога: g1.comp f = g2.comp f ⇔ g1 = g2.

LaTeX

$$$ g_1 \circ f = g_2 \circ f \iff g_1 = g_2 $ (surjective $f$).$$

Lean4

@[to_additive (attr := 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⟩

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