instDistribMulActionDomMulActOfSMulCommClass

English

Any element of a type of semilinear maps can be reinterpreted as a semilinear map by endowing it with the structure semilinearMap.

Русский

Любой элемент типа семилинейных отображений можно рассмотреть как семилинейное отображение посредством структуры semilinearMap.

LaTeX

$$semilinearMap : M \rightarrow_\sfrac{\sigma}{M_3}$$

Lean4

instance {S'} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] : DistribMulAction S'ᵈᵐᵃ (M →ₛₗ[σ₁₂] M')
    where
  one_smul _ := ext fun _ ↦ congr_arg _ (one_smul _ _)
  mul_smul _ _ _ := ext fun _ ↦ congr_arg _ (mul_smul _ _ _)
  smul_add _ _ _ := ext fun _ ↦ rfl
  smul_zero _ := ext fun _ ↦ rfl

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