monomial_zero_eq_C — Mathlib

English

The monomial of degree 0 with coefficient a equals the constant series C a.

Русский

Мономиал с степенью 0 и коэффициентом a равен константной серии C a.

LaTeX

$$$$ \operatorname{monomial}(0,a) = C(a) $$$$

Lean4

@[simp]
theorem monomial_zero_eq_C : ⇑(monomial (R := R) 0) = C := by
  -- This used to be `rw`, but we need `rw; rfl` after https://github.com/leanprover/lean4/pull/2644

  rw [monomial, Finsupp.single_zero, MvPowerSeries.monomial_zero_eq_C]
  rfl

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