eval₂_one

Mathlib.Algebra.MvPolynomial.Eval

URI: https://scilib.ai/kg/mathlib#MvPolynomial.eval₂_one

English

The evaluation of the constant 1 equals 1 in the target ring.

Русский

Оценивание единицы возвращает единицу в целевом кольце.

LaTeX

$$$\bigl(1 : \MvPolynomial\; \sigma\; R\bigr).eval_2 f g = 1$$$

Lean4

@[simp]
theorem eval₂_one : (1 : MvPolynomial σ R).eval₂ f g = 1 :=
  (eval₂_C _ _ _).trans f.map_one

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

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

Разделы

Аффилиация

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