zero_left

Mathlib.Algebra.GroupWithZero.Semiconj

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

English

For MulZeroClass, SemiconjBy 0 x y holds for all x,y.

Русский

Для MulZeroClass выполнено SemiconjBy 0 x y для всех x,y.

LaTeX

$$$SemiconjBy\ 0\ x\ y$$$

Lean4

@[simp]
theorem zero_left [MulZeroClass G₀] (x y : G₀) : SemiconjBy 0 x y := by simp only [SemiconjBy, mul_zero, zero_mul]

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

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

Разделы

Аффилиация

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