cancel_right — Mathlib

English

For any F with a FunLike structure and AlgHomClass, the RingHom obtained from the AlgHom is the same as the RingHom obtained from F.

Русский

Для любого F со структурой FunLike и AlgHomClass кольцевой гомоморфизм, полученный из AlgHom, равен кольцевому гомоморфизму из F.

LaTeX

$$$$ \mathrm{toRingHom}(\mathrm{AlgHomClass.toAlgHom} f) = \mathrm{toRingHom} f. $$$$

Lean4

theorem cancel_right {g₁ g₂ : B →ₐ[R] C} {f : A →ₐ[R] B} (hf : Function.Surjective f) :
    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => AlgHom.ext <| hf.forall.2 (AlgHom.ext_iff.1 h), fun h => h ▸ rfl⟩

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