gcd_mul_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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