of_dvd_nat

Mathlib.Algebra.Order.Ring.Abs

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

English

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

Русский

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

LaTeX

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

Lean4

theorem of_dvd_nat (hn : Odd n) (hm : m ∣ n) : Odd m :=
  not_even_iff_odd.1 <| mt hm.even (not_even_iff_odd.2 hn)

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

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

Разделы

Аффилиация

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