coe_distribMulActionHom_mk — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[norm_cast]
theorem coe_distribMulActionHom_mk (f : A →ₛₙₐ[φ] B) (h₁ h₂ h₃ h₄) :
    ((⟨⟨⟨f, h₁⟩, h₂, h₃⟩, h₄⟩ : A →ₛₙₐ[φ] B) : A →ₑ+[φ] B) = ⟨⟨f, h₁⟩, h₂, h₃⟩ := by rfl

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