even_div

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#Nat.even_div

English

Even(m/n) iff m mod (2n) / n = 0.

Русский

Чётность частного m/n эквивалентна тому, что (m mod (2n)) / n = 0.

LaTeX

$$$\\mathrm{Even}\left(\\frac{m}{n}\right) \\Leftrightarrow \\frac{m \\bmod (2n)}{n} = 0$$$

Lean4

theorem even_div : Even (m / n) ↔ m % (2 * n) / n = 0 := by
  rw [even_iff_two_dvd, dvd_iff_mod_eq_zero, ← Nat.mod_mul_right_div_self, mul_comm]

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

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

Разделы

Аффилиация

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