smeval_zero

Mathlib.Algebra.Polynomial.Laurent

URI: https://scilib.ai/kg/mathlib#LaurentPolynomial.smeval_zero

English

The evaluation of the zero Laurent polynomial is zero. For any unit x, smeval(0, x) = 0.

Русский

Оценка нулевого лаурентовского полинома равна нулю. Для любого единичного элемента x: smeval(0, x) = 0.

LaTeX

$$$ \mathrm{smeval}(0, x) = 0 $$$

Lean4

@[simp]
theorem smeval_zero : (0 : R[T;T⁻¹]).smeval x = (0 : S) := by simp only [smeval_eq_sum, Finsupp.sum_zero_index]

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

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

Разделы

Аффилиация

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