instIsIdOfIsIdCoe — Mathlib

English

If an endomorphism σ: M →* M has its underlying function equal to the identity, then σ is the identity endomorphism.

Русский

Если концевой гомоморфизм σ: M →* M имеет основанную функцию равной тождественному отображению, то σ — тождественный эндоморфизм.

LaTeX

$$$$ \sigma = \mathrm{id}_M. $$$$

Lean4

instance {σ : M →* M} [h : _root_.CompTriple.IsId σ] : IsId σ where eq_id := by ext; exact congr_fun h.eq_id _

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