coe_fst — Mathlib

English

For any a ∈ A, the first component (fst) of its image in 𝓜(𝕜, A) is left multiplication by a.

Русский

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

LaTeX

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

Lean4

@[simp, norm_cast]
theorem coe_fst (a : A) : (a : 𝓜(𝕜, A)).fst = ContinuousLinearMap.mul 𝕜 A a :=
  rfl

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