C_neg_two

Mathlib.RingTheory.Polynomial.Chebyshev

URI: https://scilib.ai/kg/mathlib#Polynomial.Chebyshev.C_neg_two

English

For any ring R, C_R(−2) = X^2 − 2.

Русский

Для любого кольца R C_R(−2) = X^2 − 2.

LaTeX

$$$ C_R(-2) = X^2 - 2 $$$

Lean4

theorem C_neg_two : C R (-2) = X ^ 2 - 2 := by simp [C_two]

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

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

Разделы

Аффилиация

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