right_div_gcd_ne_zero — Mathlib

English

Symmetrically to the left version: in a Euclidean domain, if q ≠ 0 and gcd(p,q) ≠ 0, then q / gcd(p,q) ≠ 0. This is the mirrored nonvanishing property.

Русский

Аналогично левой версии: если q ≠ 0 и gcd(p,q) ≠ 0, то q / gcd(p,q) ≠ 0. Это зеркальное свойство ненулевости.

LaTeX

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

Lean4

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

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