algebraMap_eq_inlHom — Mathlib

English

Two algebra homs from TrivSqZeroExt to A are equal if they agree on all inr-mapped elements.

Русский

Два алгебра-гомоморфизма из TrivSqZeroExt в A равны, если они совпадают на всех элементах, полученных из inr.

LaTeX

$$$ \\forall f,g : tsze R M →ₐ[S] A, \\ (\\forall m, f(inr m) = g(inr m)) \\Rightarrow f = g $$$

Lean4

theorem algebraMap_eq_inlHom : algebraMap R' (tsze R' M) = inlHom R' M :=
  rfl

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