mul_ev — Mathlib

English

Similarly to the previous case, for γ1, γ2 in OneCochain, (γ1 * γ2).ev i j a b = γ1.ev i j a b · γ2.ev i j a b.

Русский

Аналогично предыдущему: для γ1, γ2 в OneCochain, (γ1 * γ2).ev i j a b = γ1.ev i j a b · γ2.ev i j a b.

LaTeX

$$(γ1 * γ2).ev i j a b = γ1.ev i j a b · γ2.ev i j a b$$

Lean4

@[simp]
theorem mul_ev (γ₁ γ₂ : OneCochain G U) (i j : I) {T : C} (a : T ⟶ U i) (b : T ⟶ U j) :
    (γ₁ * γ₂).ev i j a b = γ₁.ev i j a b * γ₂.ev i j a b :=
  rfl

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