ofHom_v_comp_d — Mathlib

English

For φ: F ⟶ G and integers p, q, q' with hpq: p+0 = q, the composition (ofHom φ)_v(p, q, hpq) with G.d q q' equals φ_f(p) composed with G.d p q'.

Русский

Для φ: F ⟶ G и целых чисел p, q, q' с hpq: p+0 = q выполняется тождество: (ofHom φ)_v(p, q, hpq) ∘ G.d q q' = φ_f(p) ∘ G.d p q'.

LaTeX

$$$$( (\mathrm{ofHom}(\varphi)).v(p, q, hpq) ) \;\circ\; G.d(q, q') = \;\varphi_f(p) \circ G.d(p, q').$$$$

Lean4

@[simp]
theorem ofHom_v_comp_d (φ : F ⟶ G) (p q q' : ℤ) (hpq : p + 0 = q) : (ofHom φ).v p q hpq ≫ G.d q q' = φ.f p ≫ G.d p q' :=
  by simp only [ofHom, ofHoms_v_comp_d]

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