isCoprime_mul_unit_right_left

Mathlib.RingTheory.Coprime.Basic

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

← MathLib Explorer

English

If x is a unit, then IsCoprime (y x) z is equivalent to IsCoprime y z.

Русский

Если x единица, то IsCoprime (y x) z эквивалентно IsCoprime y z.

LaTeX

$$$(\text{IsUnit } x) \Rightarrow (\operatorname{IsCoprime}(y x, z) \iff \operatorname{IsCoprime}(y, z))$$$

Lean4

theorem isCoprime_mul_unit_right_left (hu : IsUnit x) (y z : R) : IsCoprime (y * x) z ↔ IsCoprime y z :=
  mul_comm x y ▸ isCoprime_mul_unit_left_left hu y z

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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