exact (sub_eq_zero.mp hb).symm
case h.e'_2.h.e'_6.e_a
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 : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑b = 0
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c) = 0
⊢ (Ideal.Quotient.mk (span {↑↑p})) ↑b = (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p)
no goals