trans_dvd

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#Even.trans_dvd

English

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

Русский

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

LaTeX

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

Lean4

theorem trans_dvd (ha : Even a) (hab : a ∣ b) : Even b :=
  even_iff_two_dvd.2 <| ha.two_dvd.trans hab

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

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

Разделы

Аффилиация

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