English
The quotient of a direct sum is the direct sum of quotients: there is a linear equivalence between the quotient of the product by Set.univ p and the product of quotients M_i/p_i.
Русский
Частоты примитивной суммы — это прямая сумма квот: существует линейное эквивалентное отображение между частной прямой суммы и произведением квот.
LaTeX
$$$\\text{quotientPi} : ((\\forall i, M_i) ⧸ pi Set.univ p) \\simeq_l[R] \\forall i, M_i/p_i$$$
Lean4
/-- The quotient of a direct sum is the direct sum of quotients. -/
@[simps!]
def quotientPi [Fintype ι] [DecidableEq ι] (p : ∀ i, Submodule R (Ms i)) :
((∀ i, Ms i) ⧸ pi Set.univ p) ≃ₗ[R] ∀ i, Ms i ⧸ p i
where
toFun := toFun p
invFun := invFun p
map_add' := map_add p
map_smul' := quotientPi_aux.map_smul p
left_inv := left_inv p
right_inv := right_inv p
