diff -r 374caac3d624 -r 125705f5965f src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Sun Sep 15 17:24:31 2019 +0200
+++ b/src/HOL/Complex.thy	Mon Sep 16 17:03:13 2019 +0100
@@ -611,6 +611,9 @@
 lemma bounded_linear_cnj: "bounded_linear cnj"
   using complex_cnj_add complex_cnj_scaleR by (rule bounded_linear_intro [where K=1]) simp
 
+lemma linear_cnj: "linear cnj"
+  using bounded_linear.linear[OF bounded_linear_cnj] .
+
 lemmas tendsto_cnj [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_cnj]
   and isCont_cnj [simp] = bounded_linear.isCont [OF bounded_linear_cnj]
   and continuous_cnj [simp, continuous_intros] = bounded_linear.continuous [OF bounded_linear_cnj]