instMul — Mathlib

English

SubMulAction R M carries a Monoid structure, with product defined via pointwise multiplication of underlying sets and the usual unit 1.

Русский

SubMulAction R M имеет структуру моноида, произведение задаётся покомпонентной умножением, единица — единица.

LaTeX

$$$\\text{SubMulAction}\\,R\\,M\\text{ is a Monoid with multiplication }(p,q) \\mapsto p*q\\text{ and }1\\text{ as unit.}$$$

Lean4

instance : Mul (SubMulAction R M) where
  mul p
    q :=
    { carrier := Set.image2 (· * ·) p q
      smul_mem' := fun r _ ⟨m₁, hm₁, m₂, hm₂, h⟩ =>
        h ▸ smul_mul_assoc r m₁ m₂ ▸ Set.mul_mem_mul (p.smul_mem _ hm₁) hm₂ }

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