of_dvd_left

Mathlib.Data.Nat.GCD.Basic

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

English

If a1 ∣ a2 and Coprime(a2,b) then Coprime(a1,b).

Русский

Если a1 делит a2 и gcd(a2,b)=1, то gcd(a1,b)=1.

LaTeX

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

Lean4

theorem of_dvd_left (ha : a₁ ∣ a₂) (h : Coprime a₂ b) : Coprime a₁ b :=
  h.coprime_dvd_left ha

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

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

Разделы

Аффилиация

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