biprod_inr_fst_f — Mathlib

English

For each i, the i-th component biprod.inr followed by the i-th component biprod.fst is zero.

Русский

Для каждого i композиция (biprod.inr)_i ∘ (biprod.fst)_i равна нулю.

LaTeX

$$$ (\mathrm{biprod.inr})_i \circ (\mathrm{biprod.fst}).f i = 0. $$$

Lean4

@[reassoc (attr := simp)]
theorem biprod_inr_fst_f (i : ι) : (biprod.inr : L ⟶ K ⊞ L).f i ≫ (biprod.fst : K ⊞ L ⟶ K).f i = 0 := by
  rw [← comp_f, biprod.inr_fst, zero_f]

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