init_neg

Mathlib.RingTheory.WittVector.InitTail

URI: https://scilib.ai/kg/mathlib#WittVector.init_neg

English

Negation commutes with init: init(n)(-x) = init(n)(-init(n)(x)).

Русский

Отрицание коммутирует с init: init(n)(-x) = init(n)(-init(n)(x)).

LaTeX

$$$$\operatorname{init}_n(-x) = \operatorname{init}_n(-\operatorname{init}_n x).$$$$

Lean4

theorem init_neg (x : 𝕎 R) (n : ℕ) : init n (-x) = init n (-init n x) := by init_ring using wittNeg_vars

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

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

Разделы

Аффилиация

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