zero_mem_centralizer

Mathlib.Algebra.GroupWithZero.Center

URI: https://scilib.ai/kg/mathlib#Set.zero_mem_centralizer

English

In a MulZeroClass, zero commutes with every element of any subset s; hence 0 ∈ centralizer s.

Русский

В MulZeroClass ноль коммутирует с любым элементом множества s; следовательно, 0 ∈ centralizer s.

LaTeX

$$$0 \in \mathrm{centralizer}(s)$$$

Lean4

@[simp]
theorem zero_mem_centralizer : (0 : M₀) ∈ centralizer s := by simp [mem_centralizer_iff]

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

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

Разделы

Аффилиация

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