gcd_mul_left — Mathlib

English

For any a in α, (s.gcd (x ↦ a · f x)) equals normalize(a) · s.gcd f.

Русский

Для любого a в α, gcd над s от функции x ↦ a · f(x) равен нормализации a, умноженной на gcd над f.

LaTeX

$$$\\forall {a \\in \\alpha}, (s.gcd\\, (\\lambda x, a \\cdot f x)) = \\mathrm{normalize}(a) \\cdot s.gcd\\, f$$$

Lean4

nonrec theorem gcd_mul_left {a : α} : (s.gcd fun x ↦ a * f x) = normalize a * s.gcd f := by
  classical
  refine s.induction_on ?_ ?_
  · simp
  · intro b t _ h
    rw [gcd_insert, gcd_insert, h, ← gcd_mul_left]
    apply ((normalize_associated a).mul_right _).gcd_eq_right

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