extract_gcd' — Mathlib

English

If there exists x in s with x ≠ 0 and s = map(s.gcd * ·) t, then t.gcd = 1.

Русский

Если существует x ∈ s с x ≠ 0 и s = map(s.gcd * ·) t, тогда t.gcd = 1.

LaTeX

$$$\exists t\ :\ \operatorname{Multiset}(\alpha),\ s = \operatorname{map}(s.\mathrm{gcd} * \cdot) t \land t.\mathrm{gcd} = 1$$$

Lean4

theorem extract_gcd' (s t : Multiset α) (hs : ∃ x, x ∈ s ∧ x ≠ (0 : α)) (ht : s = t.map (s.gcd * ·)) : t.gcd = 1 :=
  ((@mul_right_eq_self₀ _ _ s.gcd _).1 <| by conv_lhs => rw [← normalize_gcd, ← gcd_map_mul, ← ht]).resolve_right <|
    by
    contrapose! hs
    exact s.gcd_eq_zero_iff.1 hs

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