fac

Mathlib.Algebra.Category.ModuleCat.Images

URI: https://scilib.ai/kg/mathlib#ModuleCat.image.fac

English

The defining property of the image factorization states that factorThruImage f ≫ image.ι f = f.

Русский

Свойство определения факторизации изображения: factorThruImage f ≫ image.ι f = f.

LaTeX

$$$(\\mathrm{factorThruImage}\\ f) \\;\\; ≫ \\;\\; \\mathrm{image.ι}_f = f$$$

Lean4

theorem fac : factorThruImage f ≫ image.ι f = f :=
  rfl

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

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

Разделы

Аффилиация

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