two

Mathlib.Algebra.Ring.CharZero

URI: https://scilib.ai/kg/mathlib#CharZero.NeZero.two

English

In a CharZero ring, the element 2 is nonzero.

Русский

В кольце с характеристикой ноль, элемент 2 не равен нулю.

LaTeX

$$$2 \neq 0$ in CharZero ring$$

Lean4

instance two : NeZero (2 : R) where out := by rw [← Nat.cast_two, Nat.cast_ne_zero]; decide

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

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

Разделы

Аффилиация

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