init_mul

Mathlib.RingTheory.WittVector.InitTail

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

English

Similarly to addition, init(n) respects multiplication: init(n)(x y) = init(n)(init(n)(x) · init(n)(y)).

Русский

Аналогично сложению: init(n)(x y) = init(n)(init(n)(x) · init(n)(y)).

LaTeX

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

Lean4

theorem init_mul (x y : 𝕎 R) (n : ℕ) : init n (x * y) = init n (init n x * init n y) := by init_ring using wittMul_vars

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

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

Разделы

Аффилиация

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