isUnit_of_dvd'

Mathlib.RingTheory.Coprime.Basic

URI: https://scilib.ai/kg/mathlib#IsCoprime.isUnit_of_dvd'

English

If IsCoprime a b and x divides a and x divides b, then x is a unit.

Русский

Если IsCoprime a b и x делится на a и x делится на b, то x является единицей.

LaTeX

$$$IsCoprime(a,b) \land x \mid a \land x \mid b \Rightarrow IsUnit(x)$$$

Lean4

theorem isUnit_of_dvd' {a b x : R} (h : IsCoprime a b) (ha : x ∣ a) (hb : x ∣ b) : IsUnit x :=
  (h.of_isCoprime_of_dvd_left ha).isUnit_of_dvd hb

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

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

Разделы

Аффилиация

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