coe_monomial — Mathlib

English

The embedding of a monomial into the power-series ring is exactly the corresponding multivariate power-series monomial.

Русский

Встраивание мономиала в кольцо степенных рядов даёт тот же самый степенной ряд-мономиал.

LaTeX

$$$\\uparrow(\\mathrm{monomial}\\, n\\, a) = \\mathrm{MvPowerSeries.monomial}\\, n\\ a$$$

Lean4

@[simp, norm_cast]
theorem coe_monomial (n : σ →₀ ℕ) (a : R) : (monomial n a : MvPowerSeries σ R) = MvPowerSeries.monomial n a :=
  MvPowerSeries.ext fun m => by
    classical
    rw [coeff_coe, coeff_monomial, MvPowerSeries.coeff_monomial]
    split_ifs with h₁ h₂ <;>
      first
      | rfl
      | subst m; contradiction

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