| changeset 59867 | 58043346ca64 |
| parent 59862 | 44b3f4fa33ca |
| child 60017 | b785d6d06430 |
| 59866:eebe69f31474 | 59867:58043346ca64 |
|---|---|
53 |
53 |
54 end |
54 end |
55 |
55 |
56 subsection {* Multiplication and Division *} |
56 subsection {* Multiplication and Division *} |
57 |
57 |
58 instantiation complex :: field_inverse_zero |
58 instantiation complex :: field |
59 begin |
59 begin |
60 |
60 |
61 primcorec one_complex where |
61 primcorec one_complex where |
62 "Re 1 = 1" |
62 "Re 1 = 1" |
63 | "Im 1 = 0" |
63 | "Im 1 = 0" |