Theorems · Theorem · commutative algebra

Finset.gcd_div_eq_one

∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] [inst_2 : Div α]
  [MulDivCancelClass α] {f : ι → α} {s : Finset ι} {i : ι}, i ∈ s → f i ≠ 0 → (s.gcd fun j => f j / s.gcd f) = 1

Given a nonempty Finset s and a function f from s to ℕ, if d = s.gcd, then the gcd of (f i) / d is equal to 1.

Defined in

Mathlib.Algebra.GCDMonoid.Finset

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroNormalizedGCDMonoidDivMulDivCancelClass