mul_one

Mathlib.SetTheory.Nimber.Field

URI: https://scilib.ai/kg/mathlib#Nimber.mul_one

English

Multiplication by one on the right leaves a unchanged: a · 1 = a.

Русский

Умножение справа на единицу оставляет элемент без изменений: a · 1 = a.

LaTeX

$$$ a \cdot 1 = a $$$

Lean4

protected theorem mul_one (a : Nimber) : a * 1 = a := by rw [Nimber.mul_comm, Nimber.one_mul]

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

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

Разделы

Аффилиация

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