odd_of_ne_two

Mathlib.Data.Nat.Prime.Basic

URI: https://scilib.ai/kg/mathlib#Nat.Prime.odd_of_ne_two

English

If p is prime and p ≠ 2, then p is odd.

Русский

Если p простое и p ≠ 2, то p нечетное.

LaTeX

$$$$ \text{Prime}(p) \land p \neq 2 \Rightarrow \operatorname{Odd}(p). $$$$

Lean4

theorem odd_of_ne_two {p : ℕ} (hp : p.Prime) (h_two : p ≠ 2) : Odd p :=
  hp.eq_two_or_odd'.resolve_left h_two

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

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

Разделы

Аффилиация

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