instMulActionSubtypeMemSubmonoid — Mathlib

English

There is a natural MulAction instance on the unitary subtypes, giving a coherent action of unitary(R) on unitary(A).

Русский

Существует естественный экземпляр MulAction на подтипах единиц, задающий согласованное действие unitary(R) на unitary(A).

LaTeX

$$$\\text{MulAction}(\\mathrm{unitary}(R), \\mathrm{unitary}(A))$$$

Lean4

instance : MulAction (unitary R) (unitary A)
    where
  one_smul _ := Subtype.ext <| one_smul ..
  mul_smul _ _ _ := Subtype.ext <| mul_smul ..

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