English
There is a linear equivalence between the space of functions on the domain (i.e., (i : Option ι) → M i) and the product M none × (ι → M (some i)).
Русский
Существует линейное эквивалентство между пространством функций на домене (i : Option ι) и произведением M none × (ι → M (some i)).
LaTeX
$$$$ ((i:Option\\, ι) \\to M i) \\cong_{\\!R} M\\,none \\times (ι \\to M\\,(Some\\ i)) $$$$
Lean4
/-- This is `Equiv.piOptionEquivProd` as a `LinearEquiv` -/
def piOptionEquivProd {ι : Type*} {M : Option ι → Type*} [(i : Option ι) → AddCommMonoid (M i)]
[(i : Option ι) → Module R (M i)] : ((i : Option ι) → M i) ≃ₗ[R] M none × ((i : ι) → M (some i)) :=
{ Equiv.piOptionEquivProd with
map_add' := by simp [funext_iff]
map_smul' := by simp [funext_iff] }
