pow_right — Mathlib

English

If x and y are coprime in a commutative semiring, then x is coprime to every power of y: IsCoprime(x, y) implies IsCoprime(x, y^n) for all n ∈ ℕ.

Русский

Пусть x и y взаимно просты в коммутативной полукольце; тогда для любого n ∈ ℕ выполняется IsCoprime(x, y^n).

LaTeX

$$$IsCoprime(x,y) \rightarrow \forall n \in \mathbb{N},\ IsCoprime(x, y^n)$$$

Lean4

theorem pow_right (H : IsCoprime x y) : IsCoprime x (y ^ n) :=
  by
  rw [← Finset.card_range n, ← Finset.prod_const]
  exact IsCoprime.prod_right fun _ _ ↦ H

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