of_dvd_right

Mathlib.Data.Nat.GCD.Basic

URI: https://scilib.ai/kg/mathlib#Nat.Coprime.of_dvd_right

English

If b1 ∣ b2 and Coprime(a,b2) then Coprime(a,b1).

Русский

Если b1 делит b2 и gcd(a,b2)=1, то gcd(a,b1)=1.

LaTeX

$$$$\forall a,b_1,b_2 \in \mathbb{N}, b_1 \mid b_2 \land \mathrm{Coprime}(a,b_2) \Rightarrow \mathrm{Coprime}(a,b_1)$$$$

Lean4

theorem of_dvd_right (hb : b₁ ∣ b₂) (h : Coprime a b₂) : Coprime a b₁ :=
  h.coprime_dvd_right hb

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

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

Разделы

Аффилиация

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