zsmul_int_one

Mathlib.Algebra.Group.Int.Defs

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

English

For all integers n, n • 1 = n.

Русский

Для любого целого числа n верно n • 1 = n.

LaTeX

$$$\forall n\in \mathbb{Z},\ n \cdot 1 = n$$$

Lean4

theorem zsmul_int_one (n : ℤ) : n • (1 : ℤ) = n :=
  mul_one _

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

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

Разделы

Аффилиация

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