comp_one — Mathlib

English

Composition with the identity map acts as the identity on OneHom; f ∘ 1 = 1.

Русский

Композицией с единичным отображением единично действует на OneHom; f ∘ 1 = 1.

LaTeX

$$$$ \text{For } f:\ OneHom(N,P),\ f \circ 1 = 1. $$$$

Lean4

@[to_additive (attr := simp)]
theorem comp_one [One M] [One N] [One P] (f : OneHom N P) : f.comp (1 : OneHom M N) = 1 :=
  by
  ext
  simp only [OneHom.map_one, OneHom.coe_comp, Function.comp_apply, OneHom.one_apply]

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