ne_two_of_dvd_nat

Mathlib.Algebra.Order.Ring.Abs

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

← MathLib Explorer

English

If n is odd and m divides n, then m ≠ 2.

Русский

Если n нечётно и m делит n, то m не равно 2.

LaTeX

$$$$ \operatorname{Odd}(n) \land m \mid n \Rightarrow m \neq 2. $$$$

Lean4

/-- `2` is not a factor of an odd natural number. -/
theorem ne_two_of_dvd_nat {m n : ℕ} (hn : Odd n) (hm : m ∣ n) : m ≠ 2 :=
  by
  rintro rfl
  exact absurd (hn.of_dvd_nat hm) (by decide)

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

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

Разделы

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

Аффилиация

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