even

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#Dvd.dvd.even

English

If a divides b and a is even, then b is even.

Русский

Если a делит b и a чётно, то b чётно.

LaTeX

$$$\operatorname{Even}(a) \land a \mid b \Rightarrow \operatorname{Even}(b)$$$

Lean4

theorem even (hab : a ∣ b) (ha : Even a) : Even b :=
  ha.trans_dvd hab

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

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

Разделы

Аффилиация

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