coe_mul — Mathlib

English

Embedding preserves multiplication: the embedded product equals the product of embeddings.

Русский

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

LaTeX

$$$\\uparrow(\\varphi \\cdot \\psi) = (\\uparrow\\varphi) \\cdot (\\uparrow\\psi)$$$

Lean4

@[simp, norm_cast]
theorem coe_mul : ((φ * ψ : MvPolynomial σ R) : MvPowerSeries σ R) = φ * ψ :=
  MvPowerSeries.ext fun n => by classical simp only [coeff_coe, MvPowerSeries.coeff_mul, coeff_mul]

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