isUnit_of_dvd_unit

Mathlib.Algebra.Divisibility.Units

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

English

If x divides y and y is a unit, then x is a unit.

Русский

Если x делит y и y является единицей, то x является единицей.

LaTeX

$$$$x \mid y \land \operatorname{IsUnit}(y) \Rightarrow \operatorname{IsUnit}(x).$$$$

Lean4

theorem isUnit_of_dvd_unit {x y : α} (xy : x ∣ y) (hu : IsUnit y) : IsUnit x :=
  isUnit_iff_dvd_one.2 <| xy.trans <| isUnit_iff_dvd_one.1 hu

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

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

Разделы

Аффилиация

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