odd_abs — Mathlib

English

For a any element a in a linear ordered ring, the absolute value preserves oddness: Odd(|a|) iff Odd(a).

Русский

Для любого элемента a в линейно упорядоченной кольцевой группе справедливо: число с модулем нечетно тогда и только тогда, когда само число нечетно.

LaTeX

$$$\text{Odd}(|a|) \iff \text{Odd}(a)$$$

Lean4

theorem odd_abs [LinearOrder α] [Ring α] {a : α} : Odd (abs a) ↔ Odd a := by
  rcases abs_choice a with h | h <;> simp only [h, odd_neg]

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