coe_mul — Mathlib

English

The embedding map from nonnegative elements into the ambient type preserves multiplication; the product of two embedded elements equals the embedded product.

Русский

Встраивание неотрицательных элементов в внешний тип сохраняет умножение: произведение двух встроенных элементов равно встроенному произведению.

LaTeX

$$$ ((a * b) : \alpha) = a * b $$$

Lean4

@[simp, norm_cast]
protected theorem coe_mul (a b : { x : α // 0 ≤ x }) : ((a * b : { x : α // 0 ≤ x }) : α) = a * b :=
  rfl

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