Theorems · Theorem · commutative algebra

Finset.gcd_eq_gcd_filter_ne_zero

∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α} [inst_2 : DecidablePred fun x => f x = 0], s.gcd f = {x ∈ s | f x ≠ 0}.gcd f

Defined in

Mathlib.Algebra.GCDMonoid.Finset

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroNormalizedGCDMonoidDecidablePred