Theorems · Theorem · commutative algebra

Finset.extract_gcd

∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  (f : β → α), s.Nonempty → ∃ g, (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1

Defined in

Mathlib.Algebra.GCDMonoid.Finset

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroNormalizedGCDMonoid