coe_mul — Mathlib

English

The inclusion map S → A preserves multiplication: the product in S maps to the product in A under the inclusion.

Русский

Включение S → A сохраняет умножение: произведение в S отображается как произведение в A через инклюзию.

LaTeX

$$$ (x \\cdot y)^{\\uparrow} = x^{\\uparrow} \\cdot y^{\\uparrow} \\quad (x,y \\in S). $$$

Lean4

protected theorem coe_mul (x y : S) : (↑(x * y) : A) = ↑x * ↑y :=
  rfl

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