pow_left_iff — Mathlib

English

For hm > 0, IsCoprime(x^m, y) is equivalent to IsCoprime(x, y).

Русский

Пусть hm > 0. Тогда IsCoprime(x^m, y) эквивалентно IsCoprime(x, y).

LaTeX

$$$ (0 < m) \rightarrow (IsCoprime(x^m, y) \iff IsCoprime(x, y)) $$$

Lean4

theorem pow_left_iff (hm : 0 < m) : IsCoprime (x ^ m) y ↔ IsCoprime x y :=
  by
  refine ⟨fun h ↦ ?_, IsCoprime.pow_left⟩
  rw [← Finset.card_range m, ← Finset.prod_const] at h
  exact h.of_prod_left 0 (Finset.mem_range.mpr hm)

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