two_le_iff_pos_of_even

Mathlib.Algebra.Order.Ring.Int

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

English

For an even integer m, 2 ≤ m if and only if m > 0.

Русский

Для чётного целого числа m выполнено: 2 ≤ m тогда и только тогда, когда m > 0.

LaTeX

$$2 \le m \iff 0 < m, \text{when }\text{Even}(m)$$

Lean4

theorem two_le_iff_pos_of_even {m : ℤ} (even : Even m) : 2 ≤ m ↔ 0 < m :=
  le_iff_pos_of_dvd (by decide) even.two_dvd

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

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

Разделы

Аффилиация

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