init_sub

Mathlib.RingTheory.WittVector.InitTail

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

English

Init is compatible with subtraction: init(n)(x − y) = init(n)(init(n)(x) − init(n)(y)).

Русский

Init совместим с вычитанием: init(n)(x − y) = init(n)(init(n)(x) − init(n)(y)).

LaTeX

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

Lean4

theorem init_sub (x y : 𝕎 R) (n : ℕ) : init n (x - y) = init n (init n x - init n y) := by init_ring using wittSub_vars

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

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

Разделы

Аффилиация

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