coe_mul — Mathlib

English

The embedding commutes with multiplication: the embedded product equals the product of embeddings.

Русский

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

LaTeX

$$$\operatorname{coe}(x y) = (\operatorname{coe}(x)) (\operatorname{coe}(y))$$$

Lean4

@[simp, norm_cast]
theorem coe_mul (x y : R) : ↑(x * y) = (↑x * ↑y : QuadraticAlgebra R a b) := by ext <;> simp

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