rw [← one_add_one_eq_two, map_add, map_one]
p : ℕ+
K : Type ?u.154058
inst✝⁶ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁵ : NumberField K
inst✝⁴ : IsCyclotomicExtension {p} ℚ K
S : Type u_1
T : Type u_2
F : Type u_3
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring T
inst✝¹ : FunLike F S T
inst✝ : RingHomClass F S T
f : F
⊢ f 2 = 2
p : ℕ+
K : Type ?u.154058
inst✝⁶ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁵ : NumberField K
inst✝⁴ : IsCyclotomicExtension {p} ℚ K
S : Type u_1
T : Type u_2
F : Type u_3
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring T
inst✝¹ : FunLike F S T
inst✝ : RingHomClass F S T
f : F
⊢ 1 + 1 = 2