coprime_pow_of_not_dvd

Mathlib.Data.Nat.Prime.Basic

URI: https://scilib.ai/kg/mathlib#Nat.Prime.coprime_pow_of_not_dvd

English

If p is prime and p ∤ a, then Coprime a (p^m).

Русский

Пусть p — простое и p не делит a. Тогда a взаимно просто с p^m.

LaTeX

$$$$ \forall p,m,a \in \mathbb{N},\ \text{Prime}(p) \rightarrow \lnot(p \mid a) \rightarrow \mathrm{Coprime}(a, p^m). $$$$

Lean4

theorem coprime_pow_of_not_dvd {p m a : ℕ} (pp : Prime p) (h : ¬p ∣ a) : Coprime a (p ^ m) :=
  (pp.coprime_iff_not_dvd.2 h).symm.pow_right _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru