zero_right

Mathlib.Algebra.GroupWithZero.Semiconj

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

English

For any a with MulZeroClass G₀, SemiconjBy a 0 0 holds.

Русский

Для любого a в кольце с нулём выполняется SemiconjBy a 0 0.

LaTeX

$$$SemiconjBy\ a\ 0\ 0$$$

Lean4

@[simp]
theorem zero_right [MulZeroClass G₀] (a : G₀) : SemiconjBy a 0 0 := by simp only [SemiconjBy, mul_zero, zero_mul]

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

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

Разделы

Аффилиация

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