coeff_monomial_ne

Mathlib.RingTheory.MvPowerSeries.Basic

URI: https://scilib.ai/kg/mathlib#MvPowerSeries.coeff_monomial_ne

← MathLib Explorer

English

If m ≠ n, the coefficient at m of the monomial n a is 0.

Русский

Если m ≠ n, коэффициент m монома n a равен 0.

LaTeX

$$$\\text{If } m \\neq n,\\; \\mathrm{coeff}_m(\\mathrm{monomial}(n)\\, a) = 0$$$

Lean4

theorem coeff_monomial_ne {m n : σ →₀ ℕ} (h : m ≠ n) (a : R) : coeff m (monomial n a) = 0 := by
  classical
  rw [monomial_def]
  exact Pi.single_eq_of_ne h _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru