rescale_neg_one_X

Mathlib.RingTheory.PowerSeries.Basic

URI: https://scilib.ai/kg/mathlib#PowerSeries.rescale_neg_one_X

English

Replacing the scaling by -1, the indeterminate X is sent to -X; i.e., rescale(-1) X = -X.

Русский

Замена масштаба на −1 отправляет X в −X; то есть rescale(−1) X = −X.

LaTeX

$$$\\operatorname{rescale}(-1)\\,X = -X$$$

Lean4

theorem rescale_neg_one_X : rescale (-1 : A) X = -X := by rw [rescale_X, map_neg, map_one, neg_one_mul]

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

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

Разделы

Аффилиация

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