instMulActionSemiHomClassMulActionHom

English

There is a canonical instance giving that semilinear homomorphisms respect the left action, i.e., they are compatible with smul_l.

Русский

Существует канонический экземпляр, задающий совместимость полупрямых отображений с левым действием (smul).

LaTeX

$$$MulActionSemiHomClass\; (X \to_\phi[φ] Y)\ φ\ X\ Y$$$

Lean4

@[to_additive]
instance : MulActionSemiHomClass (X →ₑ[φ] Y) φ X Y where map_smulₛₗ := MulActionHom.map_smul'

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