instDistribMulActionSemiHomClassCoeMonoidHom

English

The Morphi space of homomorphisms is closed under natural coercions from F to A →ₑ+[φ] B.

Русский

Пространство гомоморфизмов замыкается на естественные приведения из F в A→ₑ+[φ]B.

LaTeX

$$$F \to (A\to_{\phi} B)$ via coercion$$

Lean4

instance : DistribMulActionSemiHomClass (A →ₑ+[φ] B) φ A B
    where
  map_smulₛₗ m := m.map_smul'
  map_zero := DistribMulActionHom.map_zero'
  map_add := DistribMulActionHom.map_add'

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