to_mulHom_injective — Mathlib

English

Equality of DistribMulActionHom representations yields equality of the original maps.

Русский

Равенство представлений DistribMulActionHom порождает равенство исходных отображений.

LaTeX

$$$\forall f,g : A \to_{\varphi} B,\; \mathrm{toDistribMulActionHom}(f) = \mathrm{toDistribMulActionHom}(g) \Rightarrow f=g$$$

Lean4

theorem to_mulHom_injective {f g : A →ₛₙₐ[φ] B} (h : (f : A →ₙ* B) = (g : A →ₙ* B)) : f = g :=
  by
  ext a
  exact DFunLike.congr_fun h a

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