simp only [map_sub, coe_unit'_coe, map_one, map_zero, sub_eq_zero] at h
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : ↑(↑hζ.unit' - 1) = ↑0
⊢ False
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : ζ = 1
⊢ False