ofHom₂_hom₂

Mathlib.Algebra.Category.ModuleCat.Basic

URI: https://scilib.ai/kg/mathlib#ModuleCat.ofHom₂_hom₂

English

The simp lemma states the same identity as above, in a simplified form for morphisms.

Русский

Смотри простое лемматическое утверждение про ту же идентичность.

LaTeX

$$$\mathrm{ofHom_2}(\mathrm{Hom_2}(f)) = f$$$

Lean4

@[simp]
theorem ofHom₂_hom₂ {M N P : ModuleCat.{u} R} (f : M ⟶ of R (N ⟶ P)) : ofHom₂ f.hom₂ = f :=
  rfl

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

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

Разделы

Аффилиация

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