gcd_div_id_eq_one — Mathlib

English

If a ∈ s and a ≠ 0 for a finite set s of α, then gcd of (b)/gcd id over b ∈ s equals 1.

Русский

Если a ∈ s и a ≠ 0 для множества s ⊆ α, то gcd элементов b, делённых на gcd id, равен 1.

LaTeX

$$$\\forall {s:\\mathrm{Finset}\\, \\alpha},\\ a\\in s,\\ a\\neq 0\\;\\Rightarrow\\ s.gcd\\ (\\lambda b, b/s.gcd\\ id) = 1$$$

Lean4

theorem gcd_div_id_eq_one {s : Finset α} {a : α} (has : a ∈ s) (ha : a ≠ 0) : s.gcd (fun b ↦ b / s.gcd id) = 1 :=
  gcd_div_eq_one has ha

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