Theorems · Theorem · commutative algebra

LocalizedModule.prod_mk

∀ {R : Type u} [inst : CommSemiring R] {ι : Type u_3} {A : Type u_4} [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  {S : Submonoid R} (t : Finset ι) (a : ι → A) (s : ι → ↥S),
  ∏ i ∈ t, LocalizedModule.mk (a i) (s i) = LocalizedModule.mk (∏ i ∈ t, a i) (∏ i ∈ t, s i)

Defined in

Mathlib.Algebra.Module.LocalizedModule.Basic

Cited by

0 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringCommSemiringAlgebra