sumArrowLequivProdArrow — Mathlib

English

There is a linear equivalence between the space of functions from Option ι to M i and the product M none × (ι → M (some i)).

Русский

Существует линейное эквивалентство между пространством функций из Option ι в M i и произведением M none × (ι → M (Some i)).

LaTeX

$$$$ ((i : Option ι) → M i) \\cong_{\\!R} M\\ none \\times \\big((i : ι) \\to M\\ (Some\\ i)\\big), $$$$

Lean4

/-- `Equiv.sumArrowEquivProdArrow` as a linear equivalence.
-/
def sumArrowLequivProdArrow (α β R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M] :
    (α ⊕ β → M) ≃ₗ[R] (α → M) × (β → M) :=
  {
    Equiv.sumArrowEquivProdArrow α β
      M with
    map_add' := by
      intro f g
      ext <;> rfl
    map_smul' := by
      intro r f
      ext <;> rfl }

Похожие утверждения