Theorems · Theorem · ring theory

TrivSqZeroExt.snd_list_prod

∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : AddCommMonoid M] [inst_2 : DistribMulAction R M]
  [inst_3 : DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (l : List (TrivSqZeroExt R M)),
  l.prod.snd =
    (List.map
        (fun x =>
          MulOpposite.op (List.drop x.2.succ (List.map TrivSqZeroExt.fst l)).prod •
            (List.take x.2 (List.map TrivSqZeroExt.fst l)).prod • x.1.snd)
        l.zipIdx).sum

The second element of a product $\prod_{i=0}^n (r_i + m_i)$ is a sum of terms of the form $r_0\cdots r_{i-1}m_ir_{i+1}\cdots r_n$.

Defined in

Mathlib.Algebra.TrivSqZeroExt.Basic

Cited by

0 results in Mathlib

Foundations

Depth 46 from the axioms · uses propext, Quot.sound

Assumes

MonoidAddCommMonoidDistribMulActionDistribMulActionSMulCommClass