English
There is a ring isomorphism between functions indexed by an option type and a product consisting of the value at none and the values at some occurrences: (Π i, R i) ≃+* R none × (Π i, R (some i)).
Русский
Существует кольцевой эквивалент между функциями, индексированными по типу Option и произведением, состоящим из значения none и значений some: (Π i, R i) ≃+* R none × (Π i, R (some i)).
LaTeX
$$$$ (\\Pi_{i:\\mathrm{Option}\\, ι} R i) \\cong+* R\\,\\mathrm{none} \\times (\\Pi_{i:ι} R(\\mathrm{Option.some}\\, i)). $$$$
Lean4
/-- This is `Equiv.piOptionEquivProd` as a `RingEquiv`. -/
@[simps!]
def piOptionEquivProd {ι : Type*} {R : Option ι → Type*} [Π i, NonUnitalNonAssocSemiring (R i)] :
(Π i, R i) ≃+* R none × (Π i, R (some i))
where
toEquiv := Equiv.piOptionEquivProd
map_add' _ _ := rfl
map_mul' _ _ := rfl
