toDistribMulActionHom — Mathlib

English

There is a formal link between semi-homomorphisms and the full homomorphisms via Coe.

Русский

Существует формальная связь между полу-гомоморфизмами и полными гомоморфизмами через приведение.

LaTeX

$$$DistribMulActionSemiHomClass F φ A B \Rightarrow F \to A\to_{φ} B$$$

Lean4

/-- Turn an element of a type `F` satisfying `MulActionHomClass F M X Y` into an actual
`MulActionHom`. This is declared as the default coercion from `F` to `MulActionHom M X Y`. -/
@[coe]
def _root_.DistribMulActionSemiHomClass.toDistribMulActionHom [DistribMulActionSemiHomClass F φ A B] (f : F) :
    A →ₑ+[φ] B :=
  { (f : A →+ B), (f : A →ₑ[φ] B) with }

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