apply_fun (fun x : 𝓞 K => (x : K))
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
⊢ ↑hζ.unit' - 1 ≠ 0
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
⊢ (fun x => ↑x) (↑hζ.unit' - 1) ≠ (fun x => ↑x) 0