not_isUnit_of_not_isUnit_dvd

Mathlib.Algebra.Divisibility.Units

URI: https://scilib.ai/kg/mathlib#not_isUnit_of_not_isUnit_dvd

English

If a is not a unit and a divides b, then b is not a unit.

Русский

Если a не единица и a делит b, то b не единица.

LaTeX

$$$$\neg\operatorname{IsUnit}(a) \land a \mid b \Rightarrow \neg \operatorname{IsUnit}(b).$$$$

Lean4

theorem not_isUnit_of_not_isUnit_dvd {a b : α} (ha : ¬IsUnit a) (hb : a ∣ b) : ¬IsUnit b :=
  mt (isUnit_of_dvd_unit hb) ha

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

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

Разделы

Аффилиация

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