instSMulZeroClass — Mathlib

English

There is a SMulZeroClass instance for units acting on α, compatible with the underlying SMulZeroClass on α via the unit's value.

Русский

Существует экземпляр SMulZeroClass для единиц, действующих на α, совместимый со структурой SMulZeroClass на α через значение единицы.

LaTeX

$$$\\text{SMulZeroClass } (Units\, M) \\; \\alpha$$$

Lean4

instance instSMulZeroClass [Monoid M] [Zero α] [SMulZeroClass M α] : SMulZeroClass Mˣ α
    where
  smul := (· • ·)
  smul_zero m := smul_zero (m : M)

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