gcd_map_mul — Mathlib

English

Multiplying every element by a fixes gcd up to normalization: gcd(map(a ·) s) = normalize(a) · gcd(s).

Русский

Умножение каждого элемента на a изменяет gcd так: gcd(map(a ·) s) = normalize(a) · gcd(s).

LaTeX

$$$(s.map (a \cdot \\cdot)).\mathrm{gcd} = \operatorname{normalize}(a) \cdot s.\mathrm{gcd}$$$

Lean4

theorem gcd_map_mul (a : α) (s : Multiset α) : (s.map (a * ·)).gcd = normalize a * s.gcd :=
  by
  refine s.induction_on ?_ fun b s ih ↦ ?_
  · simp_rw [map_zero, gcd_zero, mul_zero]
  · simp_rw [map_cons, gcd_cons, ← gcd_mul_left]
    rw [ih]
    apply ((normalize_associated a).mul_right _).gcd_eq_right

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