traverse_mul' — Mathlib

English

A derivative form of traverse_mul giving equality of two compositions with traverse of a product.

Русский

Другая форма утверждения traverse_mul, выражающая равенство двух композиций с обходом произведения.

LaTeX

$$$\operatorname{traverse} F \circ (\cdot) = \cdot \, \langle \operatorname{traverse} F, \operatorname{traverse} F \rangle$$$

Lean4

@[to_additive (attr := simp)]
theorem traverse_mul' :
    Function.comp (traverse F) ∘ (HMul.hMul : FreeSemigroup α → FreeSemigroup α → FreeSemigroup α) = fun x y ↦
      (· * ·) <$> traverse F x <*> traverse F y :=
  funext fun x ↦ funext fun y ↦ traverse_mul F x y

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