colimit_mul_mk_eq'

Mathlib.Algebra.Category.MonCat.FilteredColimits

URI: https://scilib.ai/kg/mathlib#MonCat.FilteredColimits.colimit_mul_mk_eq'

← MathLib Explorer

English

Special case: if x,y ∈ F.obj j, then

Русский

Особый случай: если x,y ∈ F.obj j, то

LaTeX

$$$M.mk F \langle j, x \rangle \;*\; M.mk F \langle j, y \rangle = M.mk F \langle j, x \cdot y \rangle$$$

Lean4

@[to_additive]
theorem colimit_mul_mk_eq' {j : J} (x y : F.obj j) :
    M.mk.{v, u} F ⟨j, x⟩ * M.mk.{v, u} F ⟨j, y⟩ = M.mk.{v, u} F ⟨j, x * y⟩ := by
  simpa using colimit_mul_mk_eq F ⟨j, x⟩ ⟨j, y⟩ j (𝟙 _) (𝟙 _)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru