Inner Products and Angles of Complex Numbers

Wenpai Chang

Shinshu University, Nagano

Yatsuka Nakamura

Shinshu University, Nagano

Piotr Rudnicki

University of Alberta, Edmonton

Summary.

An inner product of complex numbers is defined and used to characterize the (counter-clockwise) angle between ($a$,0) and (0,$b$) in the complex plane. For complex $a$, $b$ and $c$ we then define the (counter-clockwise) angle between ($a$,$c$) and ($c$, $b$) and prove theorems about the sum of internal and external angles of a triangle.

MML Identifier: COMPLEX2

Contents (PDF format)

1. Preliminaries
2. More on the Argument of a Complex Number
3. Inner Product
4. Rotation
5. Angles

Bibliography

[1] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Czeslaw Bylinski. The complex numbers. Journal of Formalized Mathematics, 2, 1990.

[3] Library Committee. Introduction to arithmetic. Journal of Formalized Mathematics, Addenda, 2003.

[4] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.

[5] Jaroslaw Kotowicz. Real sequences and basic operations on them. Journal of Formalized Mathematics, 1, 1989.

[6] Anna Justyna Milewska. The field of complex numbers. Journal of Formalized Mathematics, 12, 2000.

[7] Anna Justyna Milewska. The Hahn Banach theorem in the vector space over the field of complex numbers. Journal of Formalized Mathematics, 12, 2000.

[8] Robert Milewski. Trigonometric form of complex numbers. Journal of Formalized Mathematics, 12, 2000.

[9] Konrad Raczkowski and Pawel Sadowski. Topological properties of subsets in real numbers. Journal of Formalized Mathematics, 2, 1990.

[10] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[11] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[12] Andrzej Trybulec and Czeslaw Bylinski. Some properties of real numbers operations: min, max, square, and square root. Journal of Formalized Mathematics, 1, 1989.

[13] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.

[14] Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.

[15] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[16] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[17] Yuguang Yang and Yasunari Shidama. Trigonometric functions and existence of circle ratio. Journal of Formalized Mathematics, 10, 1998.