rw [IsCoprime]
case h
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ IsCoprime a b ↔ a + b = ⊤
case h
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ (∃ a_1 b_1, a_1 * a + b_1 * b = 1) ↔ a + b = ⊤