of_dvd_right

Mathlib.Algebra.Divisibility.Units

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

English

If IsRelPrime z y and x ∣ y then IsRelPrime z x.

Русский

Если IsRelPrime z y и x делит y, то IsRelPrime z x.

LaTeX

$$$$\operatorname{IsRelPrime}(z,y) \rightarrow (x \mid y) \rightarrow \operatorname{IsRelPrime}(z,x).$$$$

Lean4

theorem of_dvd_right (h : IsRelPrime z y) (dvd : x ∣ y) : IsRelPrime z x :=
  (h.symm.of_dvd_left dvd).symm

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

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

Разделы

Аффилиация

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