English
Split the index set by a predicate p. There is a ring isomorphism between the product over i of Y_i and the product over the subtype {i ∈ ι | p i} and the product over the complement {i ∈ ι | ¬ p i}.
Русский
Разделяем множество индексов по предикату p. Существует кольцевой эквивалент между произведением по i из ι и произведениями по подтипам {i | p i} и по комплементу {i | ¬ p i}.
LaTeX
$$$$ \\left( \\prod_{i: ι} Y_i \\right) \\cong+* \\left( \\prod_{i: { i : ι // p i }} Y_i .val \\right) \\times \\left( \\prod_{i: { i : { i : ι // ¬ p i } }} Y_i .val \\right). $$$$
Lean4
/-- Splits the indices of ring `∀ (i : ι), Y i` along the predicate `p`. This is
`Equiv.piEquivPiSubtypeProd` as a `RingEquiv`. -/
@[simps!]
def piEquivPiSubtypeProd {ι : Type*} (p : ι → Prop) [DecidablePred p] (Y : ι → Type*)
[∀ i, NonUnitalNonAssocSemiring (Y i)] :
((i : ι) → Y i) ≃+* ((i : { x : ι // p x }) → Y i) × ((i : { x : ι // ¬p x }) → Y i)
where
toEquiv := Equiv.piEquivPiSubtypeProd p Y
map_mul' _ _ := rfl
map_add' _ _ := rfl
