traverse_mul — Mathlib

English

For an applicative F and a function F : α → m β, traverse F on a product x*y equals a certain composition involving traverse F x and traverse F y and the multiplication of m.

Русский

Для применимого F и функции F: α → m β обход по произведению x·y равен композиции функций, включающей обход по x и по y и умножение в m.

LaTeX

$$$\operatorname{traverse} F (x \cdot y) = (\cdot * \cdot) <$> \operatorname{traverse} F x <*> \operatorname{traverse} F y$$$

Lean4

@[to_additive (attr := simp)]
theorem traverse_mul (x y : FreeSemigroup α) : traverse F (x * y) = (· * ·) <$> traverse F x <*> traverse F y :=
  let ⟨x, L1⟩ := x
  let ⟨y, L2⟩ := y
  List.recOn L1 (fun _ ↦ rfl)
    (fun hd tl ih x ↦
      show
        (· * ·) <$> pure <$> F x <*> traverse F (mk hd tl * mk y L2) =
          (· * ·) <$> ((· * ·) <$> pure <$> F x <*> traverse F (mk hd tl)) <*> traverse F (mk y L2)
        by rw [ih]; simp only [Function.comp_def, (mul_assoc _ _ _).symm, functor_norm])
    x

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