no goals
α : Type u_2
β : Type u_1
γ : Type ?u.40816
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hs : ∃ x, x ∈ s ∧ f x ≠ 0
hg : ∀ (b : β), b ∈ s → f b = gcd s f * g b
⊢ gcd s f * gcd s g = gcd s f
conv_lhs => rw [← normalize_gcd, ← gcd_mul_left, ← gcd_congr rfl hg]
α : Type u_2
β : Type u_1
γ : Type ?u.40816
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hg : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hs : gcd s f = 0
⊢ ∀ (x : β), x ∈ s → f x = 0
α : Type u_2
β : Type u_1
γ : Type ?u.40816
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hs : ∃ x, x ∈ s ∧ f x ≠ 0
hg : ∀ (b : β), b ∈ s → f b = gcd s f * g b
⊢ ¬gcd s f = 0
contrapose! hs
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.40816
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hg : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hs : gcd s f = 0
⊢ ∀ (x : β), x ∈ s → f x = 0
exact gcd_eq_zero_iff.1 hs