--- 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]