odd_neg

Mathlib.Algebra.Ring.Parity

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

English

In a ring, Odd(-a) is equivalent to Odd(a).

Русский

В кольце Odd(-a) эквивалентно Odd(a).

LaTeX

$$$\operatorname{Odd}(-a) \iff \operatorname{Odd}(a)$$$

Lean4

@[simp]
theorem odd_neg : Odd (-a) ↔ Odd a :=
  ⟨fun h ↦ neg_neg a ▸ h.neg, Odd.neg⟩

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

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

Разделы

Аффилиация

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