| changeset 74226 | 38c01d7e9f5b |
| parent 74223 | 527088d4a89b |
| child 75494 | eded3fe9e600 |
--- a/src/HOL/Complex.thy Fri Sep 03 22:53:11 2021 +0100 +++ b/src/HOL/Complex.thy Sat Sep 04 11:22:24 2021 +0100 @@ -26,8 +26,6 @@ lemma complex_eq_iff: "x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y" by (auto intro: complex.expand) - - subsection \<open>Addition and Subtraction\<close> instantiation complex :: ab_group_add