coprime_pow_of_not_dvd — Mathlib

English

If p is irreducible and p does not divide a, then a is coprime to p^m for any natural m.

Русский

Если p неприводимо и p не делит a, то a взаимно просто к p^m для любого натурального m.

LaTeX

$$$\forall {R} [\mathrm{CommRing}\,R] [\mathrm{IsBezout}\,R] {p a : R} (m : \mathbb{N}) (hp : \mathrm{Irreducible}(p)) (h : \neg p \mid a),\; \mathrm{IsCoprime}(a,(p^m))$$$

Lean4

theorem coprime_pow_of_not_dvd {p a : R} (m : ℕ) (hp : Irreducible p) (h : ¬p ∣ a) : IsCoprime a (p ^ m) :=
  (hp.coprime_iff_not_dvd.2 h).symm.pow_right

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