colimitMulAux — Mathlib

Lean4
/-- The "unlifted" version of multiplication in the colimit. To multiply two dependent pairs
`⟨j₁, x⟩` and `⟨j₂, y⟩`, we pass to a common successor of `j₁` and `j₂` (given by `IsFiltered.max`)
and multiply them there.
-/
@[to_additive /-- The "unlifted" version of addition in the colimit. To add two dependent pairs
          `⟨j₁, x⟩` and `⟨j₂, y⟩`, we pass to a common successor of `j₁` and `j₂`
          (given by `IsFiltered.max`) and add them there. -/
    ]
noncomputable def colimitMulAux (x y : Σ j, F.obj j) : M.{v, u} F :=
  M.mk F
    ⟨IsFiltered.max x.fst y.fst, F.map (IsFiltered.leftToMax x.1 y.1) x.2 * F.map (IsFiltered.rightToMax x.1 y.1) y.2⟩
Похожие утверждения