namespace http://mathhub.info/MitM/core/arithmetics ❚

import base http://mathhub.info/MitM/Foundation ❚

theory ComplexNumbers : base:?Logic = 
	include ?RealArithmetics ❙
	
	complexNumbers: type ❘ # ℂ ❙
	
	/T every real number is also a complex one: ❙
	axiom_realsAreComplex : ℝ <* ℂ ❙
	axiom_rationalsAreComplex : ℚ <* ℂ ❙
	axiom_integersAreComplex : ℤ <* ℂ ❙
	axiom_naturalsAreComplex : ℕ <* ℂ ❙
	axiom_posAreComplex : ℕ+ <* ℂ ❙
	// this constructor returns a complex number z with arguments Re(z), Im(z). ❙
	complexNumberConstructor: ℝ ⟶ ℝ ⟶ ℂ ❘ # 1 +i 2 ❙
	
	imaginaryUnit: ℂ ❘ = 0 +i 1 ❘ # i ❙
	/T Re returns real part of complex number. ❙
	realPart: ℂ ⟶ ℝ ❘ # Re 1 ❙
	/T Im returns real part of complex number. ❙
	imaginaryPart: ℂ ⟶ ℝ ❘ # Im 1 ❙
	/T Axioms for basic complex functions: ❙
	axiom_complexNumberConstructor_Re: ⊦ ∀[a] ∀[b] Re (a +i b) ≐ a ❙
	axiom_complexNumberConstructor_Im: ⊦ ∀[a] ∀[b] Im (a +i b) ≐ b ❙
	axiom_realPartOfReal : {x : ℝ} ⊦ x +i 0 ≐ x ❙
❚

theory ComplexArithmetic : base:?Logic =
	include ?ComplexNumbers ❙
	
	/T ComplexConjugate maps a + b i -> a - b i ❙
	complexConjugate: ℂ ⟶ ℂ ❘ = [z] (Re z) +i (- Im z) ❘ # cConj 1 ❙
	
	/T Additive Inverse ❙
	uminus : ℂ ⟶ ℂ ❘ = [x] (- Re x) +i (- Im x) ❘ # - 1 ❙
	
	/T Addition of two complex numbers ❙
	addition: ℂ ⟶ ℂ ⟶ ℂ ❘ = [z1,z2] (arithmetics?RealArithmetics?addition (Re z1) (Re z2)) +i (arithmetics?RealArithmetics?addition (Im z1) (Im z2)) ❘ # 1 + 2 ❙
		
	/T Difference of two complex numbers using additive inverse and addition ❙ 
	subtraction: ℂ ⟶ ℂ ⟶ ℂ ❘ = [z1,z2] z1 + (- z2) ❘ # 1 - 2 ❙
	
	/T Multiplication of two complex numbers with each other. ❙
	multiplication: ℂ ⟶ ℂ ⟶ ℂ ❘
													= [z1,z2] (☞?RealArithmetics?addition ((Re z1) ⋅ (Re z2)) ( ☞?RealArithmetics?uminus (Im z1) ⋅ (Im z2)))
																			 +i (☞?RealArithmetics?addition ((Re z2) ⋅ (Im z1)) ( (Re z1) ⋅ (Im z2))) ❘
													# 1 ⋅ 2 ❙
	
	/T Magnitude of  a + b i maps to sqrt(a*a+b*b)... ❙
	complexAbsoluteSquared : ℂ ⟶ ℝ ❘ = [z] Re (z ⋅ cConj z) ❘ # | 1 |^ ❙
	absolute : ℂ ⟶ ℝ ❘ = [z] sqrt (|z|^) ❘ # |1| ❙												
		
	nonzeroComplexNumbers : type ❘ # ℂ* ❘ = ⟨ z : ℂ | ⊦ Re z ≠ 0 ∨ Im z ≠ 0 ⟩❙
	inverse : ℂ* ⟶ ℂ❘ # inv 1 prec 31 ❙
	division: ℂ ⟶ ℂ* ⟶ ℂ ❘ = [u,z] u ⋅ (inv z) ❘ # 1 / 2 ❙
❚