instMulActionMulActionHomIdOfSMulCommClass

English

There is a canonical equivalence between M and its DomMulAct version Mᵈᵐᵃ, given by mk, i.e., M ≃ Mᵈᵐᵃ.

Русский

Существует каноническое эквивалентность между M и его версией DomMulAct Mᵈᵐᵃ, заданная mk, то есть M ≃ Mᵈᵐᵃ.

LaTeX

$$$M \simeq M^{\mathrm{dma}}$$$

Lean4

instance {M α N β : Type*} [Monoid M] [MulAction M α] [SMul N α] [SMulCommClass M N α] [SMul N β] :
    MulAction Mᵈᵐᵃ (α →[N] β) :=
  DFunLike.coe_injective.mulAction _ fun _ _ ↦ rfl

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