English
In a real two-dimensional oriented inner product space, the rotation by 90 degrees corresponds to multiplication by i in the corresponding complex coordinate representation: R(z) = i z for all z ∈ C.
Русский
В ориентированном вещественном двумерном пространстве с внутренним произведением поворот на 90 градусов соответствует умножению на i в комплексной записи: R(z) = i z для всех z ∈ C.
LaTeX
$$$ \\text{rightAngleRotation}(z) = i z $$$
Lean4
@[simp]
protected theorem rightAngleRotation (z : ℂ) : Complex.orientation.rightAngleRotation z = I * z :=
by
apply ext_inner_right ℝ
intro w
rw [Orientation.inner_rightAngleRotation_left]
simp only [Complex.areaForm, Complex.inner, mul_re, mul_im, conj_re, conj_im, map_mul, conj_I, neg_re, neg_im, I_re,
I_im]
ring
