isCoprime_group_smul_right

Mathlib.RingTheory.Coprime.Basic

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

← MathLib Explorer

English

With a group action, IsCoprime (x • y) z is equivalent to IsCoprime y z.

Русский

При наличии группового действия IsCoprime (x • y) z эквивалентно IsCoprime y z.

LaTeX

$$$\operatorname{IsCoprime}(x \cdot y, z) \iff \operatorname{IsCoprime}(y, z)$$$

Lean4

theorem isCoprime_group_smul_right : IsCoprime y (x • z) ↔ IsCoprime y z :=
  isCoprime_comm.trans <| (isCoprime_group_smul_left x z y).trans isCoprime_comm

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

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

Разделы

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

Аффилиация

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