left_div_gcd_ne_zero — Mathlib

English

In a Euclidean domain, if p ≠ 0 and gcd(p,q) ≠ 0, then the quotient p / gcd(p,q) is nonzero. This ensures a nontrivial reduction of p by its gcd with q.

Русский

В евклидовом домене, если p ≠ 0 и gcd(p,q) ≠ 0, то p / gcd(p,q) не равно нулю. Это гарантирует не тривиальное сокращение p на gcd(p,q).

LaTeX

$$$p \\ne 0 \\implies p / \\gcd(p,q) \\ne 0$ (при gcd(p,q) ≠ 0)$$

Lean4

theorem left_div_gcd_ne_zero {p q : R} (hp : p ≠ 0) : p / GCDMonoid.gcd p q ≠ 0 :=
  by
  obtain ⟨r, hr⟩ := GCDMonoid.gcd_dvd_left p q
  obtain ⟨pq0, r0⟩ : GCDMonoid.gcd p q ≠ 0 ∧ r ≠ 0 := mul_ne_zero_iff.mp (hr ▸ hp)
  nth_rw 1 [hr]
  rw [mul_comm, mul_div_cancel_right₀ _ pq0]
  exact r0

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