two_nsmul

Mathlib.Algebra.CharP.Two

URI: https://scilib.ai/kg/mathlib#CharTwo.two_nsmul

English

In a CharP 2 ring, the additive action of 2 annihilates every element: 2 • x = 0.

Русский

В кольце CharP 2 действие двойки на любое x даёт 0: 2 • x = 0.

LaTeX

$$$2 \\cdot x = 0 \\quad\\text{for all } x \\in R$$$

Lean4

@[scoped simp]
protected theorem two_nsmul (x : R) : 2 • x = 0 := by rw [two_smul, add_self_eq_zero]

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

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

Разделы

Аффилиация

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