coe_snd — Mathlib

English

For any a ∈ A, the second component (snd) of its image in 𝓜(𝕜, A) is the flip of the right multiplication by a.

Русский

Для любого a ∈ A вторая компонента (snd) образа a в 𝓜(𝕜, A) является перевёрнутым правым умножением на a.

LaTeX

$$$ (a : A) : (a : 𝓜(\mathbb{K}, A)).snd = (\text{ContinuousLinearMap.mul } \mathbb{K} A).flip \, a.$$$

Lean4

@[simp, norm_cast]
theorem coe_snd (a : A) : (a : 𝓜(𝕜, A)).snd = (ContinuousLinearMap.mul 𝕜 A).flip a :=
  rfl

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