isCoprime_group_smul_left — Mathlib

English

For a group action of G on R, IsCoprime(x • y, z) is equivalent to IsCoprime(y, z); the map uses the action to move the factor x to the scalar.

Русский

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

LaTeX

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

Lean4

theorem isCoprime_group_smul_left : IsCoprime (x • y) z ↔ IsCoprime y z :=
  ⟨fun ⟨a, b, h⟩ => ⟨x • a, b, by rwa [smul_mul_assoc, ← mul_smul_comm]⟩, fun ⟨a, b, h⟩ =>
    ⟨x⁻¹ • a, b, by rwa [smul_mul_smul_comm, inv_mul_cancel, one_smul]⟩⟩

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