inr_f_descShortComplex_f — Mathlib

English

For each degree n, the f-component of inr S.f composed with the f-component of descShortComplex equals the f-component of S.g.

Русский

Для каждого степени n композиция f-компоненты inr S.f с f-компонентой descShortComplex равна f-компоненте S.g.

LaTeX

$$$(inr(S.f)).f\, n \; \circ \; (descShortComplex(S)).f\, n = S.g.\!f\, n$$$

Lean4

@[reassoc (attr := simp)]
theorem inr_f_descShortComplex_f (n : ℤ) : (inr S.f).f n ≫ (descShortComplex S).f n = S.g.f n := by
  simp [descShortComplex]

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