oneHomClass — Mathlib

English

There is a canonical instance making OneHom M N a OneHomClass from M to N, i.e., maps preserving identity.

Русский

Существует каноничный экземпляр, превращающий OneHom M N в OneHomClass от M к N, то есть отображения, сохраняющие тождество.

LaTeX

$$$$ \text{OneHomClass}(\text{OneHom } M N) M N. $$$$

Lean4

@[to_additive]
instance oneHomClass : OneHomClass (OneHom M N) M N where map_one := OneHom.map_one'

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