English
The rotation by any unit circle element a is never equal to conjLIE, the complex-conjugation isometry, i.e., rotation a ≠ conjLIE for all a.
Русский
Вращение на любой элемент единичной окружности не тождественно сопряжению, то есть rotation a ≠ conjLIE.
LaTeX
$$$\forall a \in \mathbb{C}_{1},\; rotation(a) \neq conjLIE$$$
Lean4
theorem rotation_ne_conjLIE (a : Circle) : rotation a ≠ conjLIE :=
by
intro h
have h1 : rotation a 1 = conj 1 := LinearIsometryEquiv.congr_fun h 1
have hI : rotation a I = conj I := LinearIsometryEquiv.congr_fun h I
rw [rotation_apply, RingHom.map_one, mul_one] at h1
rw [rotation_apply, conj_I, ← neg_one_mul, mul_left_inj' I_ne_zero, h1, eq_neg_self_iff] at hI
exact one_ne_zero hI
