isCoprime_group_smul — Mathlib

English

For a group acting on the right, IsCoprime(y, x • z) is equivalent to IsCoprime(y, z).

Русский

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

LaTeX

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

Lean4

theorem isCoprime_group_smul : IsCoprime (x • y) (x • z) ↔ IsCoprime y z :=
  (isCoprime_group_smul_left x y (x • z)).trans (isCoprime_group_smul_right x y z)

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