to_distribMulActionHom_injective — Mathlib

English

If the underlying DistribMulActionHom representations of f and g are equal, then f = g.

Русский

Если базовые представления f и g как DistribMulActionHom равны, то f = g.

LaTeX

$$$\exists h:\, \mathrm{DistribMulActionHom}(f) = \mathrm{DistribMulActionHom}(g) \Rightarrow f=g$$$

Lean4

theorem to_distribMulActionHom_injective {f g : A →ₛₙₐ[φ] B} (h : (f : A →ₑ+[φ] B) = (g : A →ₑ+[φ] B)) : f = g :=
  by
  ext a
  exact DistribMulActionHom.congr_fun h a

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