instCoeTCOfDistribMulActionSemiHomClassCoeMonoidHom

English

There is a canonical embedding of F into the space of actual homomorphisms via toDistribMulActionHom.

Русский

Существует каноническое включение F в пространство фактических гомоморфизмов через toDistribMulActionHom.

LaTeX

$$$F \hookrightarrow (A \to_{φ} B)$ via toDistribMulActionHom$$

Lean4

/-- Any type satisfying `MulActionHomClass` can be cast into `MulActionHom`
via `MulActionHomClass.toMulActionHom`. -/
instance [DistribMulActionSemiHomClass F φ A B] : CoeTC F (A →ₑ+[φ] B) :=
  ⟨DistribMulActionSemiHomClass.toDistribMulActionHom⟩

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