theorem
proved
term proof
complex_rotation
show as:
view Lean formalization →
formal statement (Lean)
91theorem complex_rotation (z w : ℂ) :
92 -- |z × w| = |z| × |w| (scaling)
93 -- arg(z × w) = arg(z) + arg(w) modulo 2π (rotation) when both are nonzero
94 ‖z * w‖ = ‖z‖ * ‖w‖ ∧
95 (∀ hz : z ≠ 0, ∀ hw : w ≠ 0, (Complex.arg (z * w) : Real.Angle) = Complex.arg z + Complex.arg w) := by
proof body
Term-mode proof.
96 constructor
97 · exact Complex.norm_mul z w
98 · intro hz hw
99 -- Use arg_mul_coe_angle which works modulo 2π
100 exact Complex.arg_mul_coe_angle hz hw
101
102/-- **THEOREM**: 8-tick phases require rotation, which requires ℂ.
103 The first non-trivial phase (k=1) has nonzero imaginary part. -/