pow_right_iff

Mathlib.RingTheory.Coprime.Lemmas

URI: https://scilib.ai/kg/mathlib#IsRelPrime.pow_right_iff

← MathLib Explorer

English

If 0 < m, then IsRelPrime x (y^m) ↔ IsRelPrime x y.

Русский

Если 0 < m, то IsRelPrime x (y^m) ↔ IsRelPrime x y.

LaTeX

$$(0 < m) → (IsRelPrime x (y^m) ↔ IsRelPrime x y)$$

Lean4

theorem pow_right_iff (hm : 0 < m) : IsRelPrime x (y ^ m) ↔ IsRelPrime x y :=
  isRelPrime_comm.trans <| (IsRelPrime.pow_left_iff hm).trans <| isRelPrime_comm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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