Theorems · Theorem · commutative algebra

Multiset.associated_gcd_map_mul

∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α) (s : Multiset α),
  Associated (Multiset.map (fun x => a * x) s).gcd (a * s.gcd)

Defined in

Mathlib.Algebra.GCDMonoid.Multiset

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroNormalizedGCDMonoid