Theorems · Theorem · ring theory

MonoidAlgebra.prod_single

∀ {R : Type u_1} {M : Type u_4} {ι : Type u_7} [inst : CommSemiring R] [inst_1 : CommMonoid M] (s : Finset ι)
  (m : ι → M) (r : ι → R),
  ∏ i ∈ s, MonoidAlgebra.single (m i) (r i) = MonoidAlgebra.single (∏ i ∈ s, m i) (∏ i ∈ s, r i)

Defined in: Mathlib.Algebra.MonoidAlgebra.Defs
Cited by: 1 results in Mathlib
Foundations: Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring CommMonoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Finsetstatement and proof · cited by 13,712
CommSemiringstatement and proof · cited by 10,911
Finset.prodstatement and proof · cited by 2,356
CommMonoidstatement and proof · cited by 2,264
MonoidAlgebrastatement and proof · cited by 590
MonoidAlgebra.singlestatement and proof · cited by 253
Finset.consproof · cited by 221
Finset.prod_consproof · cited by 60
Finset.cons_induction_onproof · cited by 37
MonoidAlgebra.single_mul_singleproof · cited by 14

Cited by1

Results whose statement or proof uses this declaration.

MonoidAlgebra.finsuppProd_singleproof · cited by 0