zero_left

Mathlib.Algebra.GroupWithZero.Commute

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

English

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

Русский

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

LaTeX

$$$Commute 0 a$$$

Lean4

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

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

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

Разделы

Аффилиация

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