d_comp_ofHom_v — Mathlib

English

For φ: F ⟶ G and p', p, q with hpq: p+0 = q, the left and right compositions with F.d commute: F.d p' p ∘ (ofHom φ)_v(p, q, hpq) = F.d p' q ∘ φ_f(q).

Русский

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

LaTeX

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

Lean4

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

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