one_left

Mathlib.Algebra.Group.Commute.Defs

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

English

The element a commutes with the unit 1: 1 * a = a * 1.

Русский

Единица 1 коммутирует с элементом a: 1·a = a·1.

LaTeX

$$$\\forall a \\in M,\\ Commute 1 a$$$

Lean4

@[to_additive (attr := simp)]
theorem one_left (a : M) : Commute 1 a :=
  SemiconjBy.one_left a

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

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

Разделы

Аффилиация

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