abs_left_iff — Mathlib

English

Let R be a commutative ring with a linear order and AddLeftMono. For all x,y in R, IsCoprime(|x|, y) if and only if IsCoprime(x, y).

Русский

Пусть R – коммутативное кольцо с линейным порядком и AddLeftMono. Для любых x,y ∈ R выполняется: IsCoprime(|x|, y) эквивалентно IsCoprime(x, y).

LaTeX

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

Lean4

theorem abs_left_iff (x y : R) : IsCoprime |x| y ↔ IsCoprime x y := by
  cases le_or_gt 0 x with
  | inl h => rw [abs_of_nonneg h]
  | inr h => rw [abs_of_neg h, IsCoprime.neg_left_iff]

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