smul_mem_trW_iff

Mathlib.CategoryTheory.Triangulated.Subcategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.smul_mem_trW_iff

← MathLib Explorer

English

For a morphism f and a unit n, P.trW (n • f) is equivalent to P.trW f.

Русский

Для морфизма f и элемента-единицы n: P.trW (n • f) эквивалентно P.trW f.

LaTeX

$$$P.trW (n \\cdot f) \\quad\\Leftrightarrow\\quad P.trW f$$

Lean4

theorem smul_mem_trW_iff {X Y : C} (f : X ⟶ Y) (n : ℤˣ) : P.trW (n • f) ↔ P.trW f :=
  P.trW.arrow_mk_iso_iff (Arrow.isoMk (n • (Iso.refl _)) (Iso.refl _))

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

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

Разделы

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

Аффилиация

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