mul_bind — Mathlib

English

The multiplication interacts with bind as x · y >>= f = (x >>= f) · (y >>= f); i.e., bind distributes over multiplication.

Русский

Умножение взаимодействует с связыванием так: x · y >>= f = (x >>= f) · (y >>= f).

LaTeX

$$$x \cdot y \gg= f = (x \gg= f) \cdot (y \gg= f)$$$

Lean4

@[to_additive (attr := simp)]
theorem mul_bind (f : α → FreeSemigroup β) (x y : FreeSemigroup α) : x * y >>= f = (x >>= f) * (y >>= f) :=
  map_mul (lift f) _ _

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