English
The product over S ⊕ T of a family of modules is linearly isomorphic to the product over S of A(inl) together with the product over T of A(inr). This is the linear version of Equiv.sumPiEquivProdPi.
Русский
Произведение по S ⊕ T от семейства модулей линейно изоморфно произведению по S от A(inl) и по T от A(inr). Это линейная версия Equiv.sumPiEquivProdPi.
LaTeX
$$$ \Big( \prod_{st:\,S\oplus T} A\,st \Big) \simeq_{[R]} \Big( \prod_{s:\,S} A(\mathrm{inl}(s)) \Big) \times \Big( \prod_{t:\,T} A(\mathrm{inr}(t)) \Big)$$$
Lean4
/-- 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`.
-/
@[simps -fullyApplied +simpRhs]
def sumPiEquivProdPi (R : Type*) [Semiring R] (S T : Type*) (A : S ⊕ T → Type*) [∀ st, AddCommMonoid (A st)]
[∀ st, Module R (A st)] : (Π (st : S ⊕ T), A st) ≃ₗ[R] (Π (s : S), A (.inl s)) × (Π (t : T), A (.inr t))
where
__ := Equiv.sumPiEquivProdPi _
map_add' _ _ := rfl
map_smul' _ _ := rfl
