Theorems · Definition · commutative algebra

Finset.lcm

{α : Type u_2} → {β : Type u_3} → [inst : CommMonoidWithZero α] → [NormalizedGCDMonoid α] → Finset β → (β → α) → α

Least common multiple of a finite set

Defined in

Mathlib.Algebra.GCDMonoid.Finset

Cited by

37 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroNormalizedGCDMonoid