odd_coe_nat

Mathlib.Algebra.Ring.Int.Parity

URI: https://scilib.ai/kg/mathlib#Int.odd_coe_nat

English

For every natural number n, Odd(n as an integer) is equivalent to Odd n.

Русский

Для любого натурального числа n нечетность (n как целое) эквивалентна нечетности n.

LaTeX

$$$\\operatorname{Odd}(n_{\\mathbb{Z}}) \\iff \\operatorname{Odd}(n)$$$

Lean4

@[simp, norm_cast]
theorem odd_coe_nat (n : ℕ) : Odd (n : ℤ) ↔ Odd n := by grind

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

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

Разделы

Аффилиация

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