zsmul_int_int

Mathlib.Algebra.Group.Int.Defs

URI: https://scilib.ai/kg/mathlib#zsmul_int_int

English

For all integers a,b, a • b = a × b.

Русский

Для любых целых чисел a и b верно, что a • b = a b.

LaTeX

$$$\forall a,b\in \mathbb{Z},\ a\cdot b = a b$$$

Lean4

theorem zsmul_int_int (a b : ℤ) : a • b = a * b :=
  rfl

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

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

Разделы

Аффилиация

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