coe_monomial — Mathlib

English

The coercion of a monomial equals the formal power series monomial: (monomial n a : PowerSeries R) = PowerSeries.monomial n a.

Русский

Приведение мононима к степенному ряду даёт точное соответствие: (monomial n a) в PowerSeries = PowerSeries.monomial n a.

LaTeX

$$$(\\operatorname{monomial} n a : PowerSeries R) = \\PowerSeries.monomial n a$$$

Lean4

@[simp, norm_cast]
theorem coe_monomial (n : ℕ) (a : R) : (monomial n a : PowerSeries R) = PowerSeries.monomial n a :=
  by
  ext
  simp [coeff_coe, PowerSeries.coeff_monomial, Polynomial.coeff_monomial, eq_comm]

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