Theorem: FltRegular.Int.gcd_left_comm (FltRegular/CaseII/Statement.lean)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
a b c : ℤ
⊢ a.gcd ↑(b.gcd c) = b.gcd ↑(a.gcd c)
Tactic:
rw [← Int.gcd_assoc, ← Int.gcd_assoc, Int.gcd_comm a b]
State after:
no goals