lift_of_mul

Mathlib.Algebra.Free

URI: https://scilib.ai/kg/mathlib#FreeSemigroup.lift_of_mul

English

For any x,y in α, lift f (of x * y) = f x * lift f y; i.e., lifting preserves multiplication.

Русский

Для любых x, y из α: lift f (of x * y) = f x * lift f y; то есть лифтинг сохраняет умножение.

LaTeX

$$$\text{lift } f (\text{of } x * \text{of } y) = f x * \text{lift } f y$$$

Lean4

@[to_additive]
theorem lift_of_mul (x y) : lift f (of x * y) = f x * lift f y := by rw [map_mul, lift_of]

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

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

Разделы

Аффилиация

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