rw [mem_span_singleton]
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
x y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ↑↑p * r ∈ span {↑↑p}
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
x y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ↑↑p ∣ ↑↑p * r