α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
b c : α
⊢ gcd (0 * b) (0 * c) = ↑normalize 0 * gcd b c
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b c : α
⊢ a = 0 → gcd (a * b) (a * c) = ↑normalize a * gcd b c
rintro rfl
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
b c : α
⊢ gcd (0 * b) (0 * c) = ↑normalize 0 * gcd b c
simp only [zero_mul, gcd_zero_left, normalize_zero]
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b c : α
ha : a ≠ 0
this : gcd (a * b) (a * c) = ↑normalize (a * gcd b c)
⊢ gcd (a * b) (a * c) = ↑normalize a * gcd b c
simpa