coeAddMonoidHom_of — Mathlib

English

The coordinatewise embedding commutes with the i-th direct sum of the i-th component: DirectSum.coeAddMonoidHom A (of (fun i => A i) i x) = x.

Русский

Координатное вложение и i-я вставка в прямой сумме commute: DirectSum.coeAddMonoidHom A (of (fun i => A i) i x) = x.

LaTeX

$$$$\\operatorname{DirectSum.coeAddMonoidHom} A\\; (\\operatorname{DirectSum.of}(\\lambda i\\mapsto A(i))\; i\\; x) = x.$$$$

Lean4

@[simp]
theorem coeAddMonoidHom_of {M S : Type*} [DecidableEq ι] [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M]
    (A : ι → S) (i : ι) (x : A i) : DirectSum.coeAddMonoidHom A (of (fun i => A i) i x) = x :=
  toAddMonoid_of _ _ _

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