of_dvd_left

Mathlib.Algebra.Divisibility.Units

URI: https://scilib.ai/kg/mathlib#IsRelPrime.of_dvd_left

Lean4

theorem of_dvd_left (h : IsRelPrime y z) (dvd : x ∣ y) : IsRelPrime x z := by obtain ⟨d, rfl⟩ := dvd;
  exact IsRelPrime.of_mul_left_left h

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

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

Разделы

Аффилиация

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