fst_list_prod — Mathlib

English

Two monoid structures defined on tsze_R M coincide; in particular, the canonical monoid isomorphism identifies them.

Русский

Два определения моноида на tsze_R M совпадают; в частности каноническое моноидальное изоморство их отождествляет.

LaTeX

$$$ tsze_R M = tsze_R M$$$

Lean4

theorem fst_list_prod [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M]
    (l : List (tsze R M)) : l.prod.fst = (l.map fst).prod :=
  map_list_prod ({ toFun := fst, map_one' := fst_one, map_mul' := fst_mul } : tsze R M →* R) _

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