instIsCocomm — Mathlib

English

If IsCocomm holds for each A_i, then the Finsupp structure is IsCocomm.

Русский

Если справедливо IsCocomm для каждой A_i, то Finsupp обладает IsCocomm.

LaTeX

$$$\text{IsCocomm}_{R}(\iota \to A_i)$ under the appropriate Triple conditions.$$

Lean4

instance instIsCocomm [IsCocomm R A] : IsCocomm R (ι →₀ A) where
  comm_comp_comul :=
    by
    ext i : 1
      -- TODO: Add `reassoc` for `LinearMap`. Then we wouldn't need to reassociate back and forth.

    simp only [comp_assoc, comul_comp_lsingle]
    simp only [← comp_assoc, ← TensorProduct.map_comp_comm_eq]
    simp [LinearMap.comp_assoc]

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