In this article, we define the division of the quaternion numbers, we also give the definition of inner products, group, ring of the quaternion numbers, and we prove some of their properties.MML identifier: QUATERN2, version: 7.8.10 4.100.1011
@article{bwmeta1.element.doi-10_2478_v10037-008-0019-x, author = {Fuguo Ge}, title = {Inner Products, Group, Ring of Quaternion Numbers}, journal = {Formalized Mathematics}, volume = {16}, year = {2008}, pages = {135-139}, language = {en}, url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_2478_v10037-008-0019-x} }
Fuguo Ge. Inner Products, Group, Ring of Quaternion Numbers. Formalized Mathematics, Tome 16 (2008) pp. 135-139. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_2478_v10037-008-0019-x/
[1] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990.
[2] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175-180, 1990.
[3] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990.
[4] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35-40, 1990.
[5] Xiquan Liang and Fuguo Ge. The quaternion numbers. Formalized Mathematics, 14(4):161-169, 2006.
[6] Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445-449, 1990.
[7] Wojciech A. Trybulec. Groups. Formalized Mathematics, 1(5):821-827, 1990.
[8] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990.
[9] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.