inl_v_desc_f — Mathlib

English

For all integers p,q with h : p + (−1) = q, we have (inl φ).v p q h is a linear map such that (inl φ).v p q h followed by the f-component of desc φ α β eq equals α.v p q h.

Русский

Для целых p, q с условием h: p + (−1) = q, выполняется, что (inl φ).v p q h последовательность за этим следует коэффициенту desc φ α β eq, равному α.v p q h.

LaTeX

$$$(\mathrm{inl}(\phi))_v(p,q,h) \circ (\desc(\phi, \alpha, \beta, eq))_f(q) = α_v(p,q,h)$$$

Lean4

@[reassoc (attr := simp)]
theorem inl_v_desc_f (p q : ℤ) (h : p + (-1) = q) : (inl φ).v p q h ≫ (desc φ α β eq).f q = α.v p q h := by simp [desc]

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