odd_neg_one

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#odd_neg_one

English

In a ring, Odd(-1).

Русский

В кольце, нечетность −1.

LaTeX

$$$\operatorname{Odd}(-1)$$$

Lean4

theorem odd_neg_one : Odd (-1 : α) := by simp

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

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

Разделы

Аффилиация

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