English
If ι has a unique element, then the evaluation map (ι → M) → M is a linear equivalence (ι → M) ≃_R M.
Русский
Если индексация ι имеет уникальный элемент, то отображение оценки является линейным эквивалентоством между (ι → M) и M.
LaTeX
$$$$ (\\text{funUnique } ι\\, R\\, M) : (ι \\to M) \\simeq_{R} M, $$$$
Lean4
/-- Linear equivalence between dependent functions `(i : Fin 2) → M i` and `M 0 × M 1`. -/
@[simps +simpRhs -fullyApplied symm_apply]
def piFinTwo (M : Fin 2 → Type v) [(i : Fin 2) → AddCommMonoid (M i)] [(i : Fin 2) → Module R (M i)] :
((i : Fin 2) → M i) ≃ₗ[R] M 0 × M 1 :=
{ piFinTwoEquiv M with
map_add' := fun _ _ => rfl
map_smul' := fun _ _ => rfl }
