Theorems · Theorem · commutative algebra

Finset.gcd_mul_left

∀ {β : Type u_3} {α : Type u_5} [inst : CommMonoidWithZero α] [inst_1 : StrongNormalizedGCDMonoid α] {s : Finset β}
  {f : β → α} {a : α}, (s.gcd fun x => a * f x) = normalize a * s.gcd f

Defined in

Mathlib.Algebra.GCDMonoid.Finset

Cited by

2 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidWithZeroStrongNormalizedGCDMonoid