isIso_r

Mathlib.CategoryTheory.Abelian.NonPreadditive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.NonPreadditiveAbelian.isIso_r

English

The morphism r A is an isomorphism: r A ≅ 1.

Русский

Отображение r A является изоморфизмом.

LaTeX

$$$\\operatorname{IsIso}(\\mathrm{r}\\ A)$$$

Lean4

instance isIso_r {A : C} : IsIso (r A) :=
  isIso_of_mono_of_epi _

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

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

Разделы

Аффилиация

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