rw [← map_one <| algebraMap A <| A ⧸ Ideal.span ({t - 1} : Set A), ← sub_eq_zero, ← map_sub,
  Ideal.Quotient.algebraMap_eq, Ideal.Quotient.eq_zero_iff_mem]
p : ℕ+
K : Type ?u.53883
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
A : Type u_1
inst✝ : CommRing A
t : A
⊢ (algebraMap A (A ⧸ Ideal.span {t - 1})) t = 1
p : ℕ+
K : Type ?u.53883
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
A : Type u_1
inst✝ : CommRing A
t : A
⊢ t - 1 ∈ Ideal.span {t - 1}