eq_C_of_isEmpty

Mathlib.Algebra.MvPolynomial.Basic

URI: https://scilib.ai/kg/mathlib#MvPolynomial.eq_C_of_isEmpty

English

The coefficient functional for a constant C a, gives coeff m (C a) = if 0=m then a else 0.

Русский

Коэффициент для константы: coeff m (C a) = if 0 = m then a else 0.

LaTeX

$$$\mathrm{coeff}\;m (C\;a) = \mathrm{if}\ 0=m\ \mathrm{then}\ a\ \mathrm{else}\ 0$$$

Lean4

theorem eq_C_of_isEmpty [IsEmpty σ] (p : MvPolynomial σ R) : p = C (p.coeff 0) :=
  by
  obtain ⟨x, rfl⟩ := C_surjective σ p
  simp

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

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

Разделы

Аффилиация

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