isRelPrime_mul_unit_right_left

Mathlib.Algebra.Divisibility.Units

URI: https://scilib.ai/kg/mathlib#isRelPrime_mul_unit_right_left

English

Let x be a unit. Then IsRelPrime(y·x, z) is equivalent to IsRelPrime(y, z).

Русский

Пусть x — единица. Тогда IsRelPrime(y·x, z) равносильно IsRelPrime(y, z).

LaTeX

$$$\text{IsUnit}(x) \implies \text{IsRelPrime}(y \cdot x, z) \iff \text{IsRelPrime}(y, z)$$$

Lean4

theorem isRelPrime_mul_unit_right_left : IsRelPrime (y * x) z ↔ IsRelPrime y z := by
  rw [mul_comm, isRelPrime_mul_unit_left_left hu]

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

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

Разделы

Аффилиация

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