of_dvd

Mathlib.Data.Nat.GCD.Basic

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

English

If a1 ∣ a2 and b1 ∣ b2 and Coprime(a2,b2) then Coprime(a1,b1).

Русский

Если a1|a2 и b1|b2 и gcd(a2,b2)=1, то gcd(a1,b1)=1.

LaTeX

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

Lean4

theorem of_dvd (ha : a₁ ∣ a₂) (hb : b₁ ∣ b₂) (h : Coprime a₂ b₂) : Coprime a₁ b₁ :=
  (h.of_dvd_left ha).of_dvd_right hb

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

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

Разделы

Аффилиация

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