zero_right

Mathlib.Algebra.GroupWithZero.Commute

URI: https://scilib.ai/kg/mathlib#Commute.zero_right

English

For any G₀ with MulZeroClass, a commutes with 0: a · 0 = 0 · a.

Русский

Для любой структуры с умножением и нулём, элемент a коммутирует с 0: a·0 = 0·a.

LaTeX

$$$Commute a 0$$$

Lean4

@[simp]
theorem zero_right [MulZeroClass G₀] (a : G₀) : Commute a 0 :=
  SemiconjBy.zero_right a

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

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

Разделы

Аффилиация

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