abs_right

Mathlib.RingTheory.Coprime.Basic

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

English

In a linearly ordered ring with AddLeftMono, if x and y are coprime, then x is coprime to |y|.

Русский

В упорядоченном по линейному порядку кольце с AddLeftMono, если x и y взаимно просты, то x взаимно просто с |y|.

LaTeX

$$$\\text{IsCoprime}(x,y) \\Rightarrow \\text{IsCoprime}(x,|y|)$$$

Lean4

theorem abs_right {x y : R} (h : IsCoprime x y) : IsCoprime x |y| :=
  abs_right_iff _ _ |>.2 h

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

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

Разделы

Аффилиация

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