mod_even

Mathlib.Algebra.Order.Ring.Abs

URI: https://scilib.ai/kg/mathlib#Odd.mod_even

← MathLib Explorer

English

If n is odd and a is even, then n mod a is odd.

Русский

Если n нечётно и a чётно, то n mod a нечётно.

LaTeX

$$$$ \operatorname{Odd}(n) \land \operatorname{Even}(a) \Rightarrow \operatorname{Odd}(n \bmod a). $$$$

Lean4

/-- If `n` is odd and `a` is even, then `n % a` is odd. -/
theorem mod_even (hn : Odd n) (ha : Even a) : Odd (n % a) :=
  (Odd.mod_even_iff ha).mpr hn

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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