odd_mul

Mathlib.Algebra.Ring.Int.Parity

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

English

For integers m, n, Odd(mn) holds iff both m and n are odd.

Русский

Для целых m, n число mn нечетно тогда и только тогда, когда оба множителя нечетные.

LaTeX

$$$\\operatorname{Odd}(m n) \\iff (\\operatorname{Odd} m \\wedge \\operatorname{Odd} n)$$$

Lean4

theorem odd_mul : Odd (m * n) ↔ Odd m ∧ Odd n := by simp [← not_even_iff_odd, not_or, parity_simps]

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

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

Разделы

Аффилиация

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