coe_mul — Mathlib

English

The embedding preserves multiplication: for a,b ∈ α, the image of ab equals the product of images.

Русский

Встраивание сохраняет умножение: для a,b ∈ α изображение ab равно произведению изображений.

LaTeX

$$$\\operatorname{coe}'(ab) = \\operatorname{coe}'(a) \\operatorname{coe}'(b)$$$

Lean4

@[norm_cast]
theorem coe_mul (a b : α) : ((a * b : α) : Completion α) = a * b :=
  ((isDenseInducing_coe.prodMap isDenseInducing_coe).extend_eq ((continuous_coe α).comp (@continuous_mul α _ _ _))
      (a, b)).symm

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