Theorems · Definition · commutative algebra

LinearEquiv.sumPiEquivProdPi

(R : Type u_9) →
  [inst : Semiring R] →
    (S : Type u_10) →
      (T : Type u_11) →
        (A : S ⊕ T → Type u_12) →
          [inst_1 : (st : S ⊕ T) → AddCommMonoid (A st)] →
            [inst_2 : (st : S ⊕ T) → Module R (A st)] →
              ((st : S ⊕ T) → A st) ≃ₗ[R] ((s : S) → A (Sum.inl s)) × ((t : T) → A (Sum.inr t))

The product over S ⊕ T of a family of modules is isomorphic to the product of (the product over S) and (the product over T). This is Equiv.sumPiEquivProdPi as a LinearEquiv.

Defined in

Mathlib.Algebra.Module.Equiv.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModule