coe_mul — Mathlib

English

The coercion from SignType to α preserves multiplication: the product maps to the product in α under the cast homomorphism.

Русский

Переход из SignType в α сохраняет умножение: произведение отображается в произведение в α через гомоморфизм приведения.

LaTeX

$$$\uparrow(a \cdot b) = (\uparrow a) \cdot (\uparrow b)$$$

Lean4

@[simp, norm_cast]
theorem coe_mul {α} [MulZeroOneClass α] [HasDistribNeg α] (a b : SignType) : ↑(a * b) = (a : α) * b :=
  map_mul SignType.castHom _ _

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