Theorems · Theorem · commutative algebra
Finset.gcd_eq_sum_mul
∀ {R : Type u} {α : Type u_1} [inst : CommRing R] [IsBezout R] [inst_2 : NormalizedGCDMonoid R] (s : Finset α)
(f : α → R), ∃ g, s.gcd f = ∑ a ∈ s, f a * g aA version of Bézout's lemma for greatest common divisors over arbitrary Finsets.
- Defined in
- Mathlib.RingTheory.PrincipalIdealDomain
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites23
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Finsetstatement and proof · cited by 13,712
- Finset.sumstatement and proof · cited by 5,195
- Unitsproof · cited by 2,804
- Finset.sum_congrproof · cited by 2,323
- mul_commproof · cited by 2,262
- Units.valproof · cited by 1,966
- mul_assocproof · cited by 1,667
- Function.updateproof · cited by 502
- add_mulproof · cited by 363
- Function.update_selfproof · cited by 201
- Function.update_of_neproof · cited by 198
Cited by1
Results whose statement or proof uses this declaration.
- Rat.iSup_finitePlace_apply_eq_one_of_gcd_eq_oneproof · cited by 1