of_mul

Mathlib.GroupTheory.FreeAbelianGroup

URI: https://scilib.ai/kg/mathlib#FreeAbelianGroup.of_mul

English

There is a canonical multiplication on FreeAbelianGroup α satisfying of(xy) = of(x) · of(y).

Русский

Существует каноничное умножение на FreeAbelianGroup α, удовлетворяющее of(xy) = of(x) · of(y).

LaTeX

$$$\operatorname{of}(x y) = \operatorname{of}(x) \cdot \operatorname{of}(y)$$$

Lean4

theorem of_mul (x y : α) : of (x * y) = of x * of y :=
  Eq.symm <| of_mul_of x y

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

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

Разделы

Аффилиация

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