abs_right_iff

Mathlib.RingTheory.Coprime.Basic

URI: https://scilib.ai/kg/mathlib#IsCoprime.abs_right_iff

English

IsCoprime x |y| iff IsCoprime x y.

Русский

IsCoprime x |y| эквивалентно IsCoprime x y.

LaTeX

$$$\operatorname{IsCoprime}(x, |y|) \iff \operatorname{IsCoprime}(x, y)$$$

Lean4

theorem abs_right_iff (x y : R) : IsCoprime x |y| ↔ IsCoprime x y := by
  rw [isCoprime_comm, IsCoprime.abs_left_iff, isCoprime_comm]

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

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

Разделы

Аффилиация

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