mul_snd — Mathlib

English

Let a and b be elements of the multiplier algebra 𝓜(𝕜, A). The second coordinate of their product equals the product (in the reverse order) of their second coordinates: (a b).snd = b.snd ∘ a.snd.

Русский

Пусть a и b — элементы умножителя 𝓜(𝕜, A). Второй координатный компонент их произведения равен композиции их вторых координат в обратном порядке: (a b).snd = b.snd ∘ a.snd.

LaTeX

$$$ (a b).snd = b.snd \\circ a.snd $$$

Lean4

@[simp]
theorem mul_snd (a b : 𝓜(𝕜, A)) : (a * b).snd = b.snd * a.snd :=
  rfl

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