# Zulip Chat Archive

## Stream: new members

### Topic: Rotation ≠ Reflection

#### Shadman Sakib (Jul 16 2021 at 22:19):

I'm working on a lemma that shows a rotation by $\theta$ is never the same as a reflection about the x-axis. Simplified to an equation, I am trying to prove $e^{i\theta}*z ≠ \bar{z}$. I found an example of z for which this equation is not true, but I am having trouble finishing the proof.

#### Shadman Sakib (Jul 16 2021 at 22:20):

```
import analysis.complex.isometry
import analysis.special_functions.trigonometric
noncomputable theory
open complex
local notation `π` := real.pi
lemma reflection_rotation : ∀ θ, ∃ z, rotation (exp_map_circle θ) z ≠ conj_lie z :=
begin
intro θ,
simp,
use exp(I * (- (θ/2) + 2)),
rw ← exp_conj,
rw conj.map_mul,
simp,
rw conj.map_div,
simp,
rw ← exp_add,
rw mul_add,
rw ← add_assoc,
have : ↑θ * I + I * -(↑θ/2) = I * (θ/2),
{ ring, },
rw this,
simp,
rw add_comm,
rw exp_eq_exp_iff_exists_int,
sorry,
end
```

#### Shadman Sakib (Jul 16 2021 at 22:21):

How can I show that there is, in fact, not an $n \in \Z$ that satisfies the equation or that the equation before I rewrite exp_eq_exp_iff_exists_int is, in fact, false?

#### Notification Bot (Jul 16 2021 at 22:45):

Shadman Sakib has marked this topic as resolved.

#### Notification Bot (Jul 16 2021 at 22:46):

Shadman Sakib has marked this topic as unresolved.

#### Eric Rodriguez (Jul 16 2021 at 23:23):

```
push_neg,
ring,
intros n h,
replace h := add_left_cancel (mul_right_cancel' I_ne_zero h),
```

will get you closer to your goal. a word of advice, though, using`simp`

every line is slow + bad style (what if someone adds a new simp lemma? then it could break your whole proof). try use `squeeze_simp`

if `simp`

doesn't finish your goal and replace the `simp`

with the `simp only`

it suggests

#### Eric Rodriguez (Jul 16 2021 at 23:24):

you can also group `rw`

s using the syntax `rw [add_comm, exp_eq_exp_iff_exists_int]`

(for example)

#### Eric Rodriguez (Jul 16 2021 at 23:25):

it'd be interesting, but not sure if possible in mathlib, to prove this via complex diffability; the lhs is complex diffable whilst the rhs isn't

#### Kyle Miller (Jul 16 2021 at 23:37):

@Shadman Sakib Sometimes it pays to generalize a lemma to prove a more specialized one:

```
import analysis.complex.isometry
noncomputable theory
open complex
lemma reflection_rotation' (w : ℂ) : ∃ z, ¬ w * z = conj z :=
begin
by_cases hu : w.re = -1,
{ use 1,
simp only [mul_one, ring_hom.map_one],
rintro rfl,
rw one_re at hu,
linarith, },
{ use I,
rw [conj_I, ←add_left_inj I, neg_add_self],
nth_rewrite 1 ←one_mul I,
rw [←right_distrib, mul_eq_zero],
simp only [I_ne_zero, or_false],
rw ←add_left_inj (-1 : ℂ),
simp only [add_neg_cancel_right, zero_add],
rintro rfl,
simpa using hu, }
end
lemma reflection_rotation (θ : ℝ) : ∃ z, rotation (exp_map_circle θ) z ≠ conj_lie z :=
begin
simp only [rotation_apply, ne.def, conj_lie_apply],
exact reflection_rotation' (exp_map_circle θ),
end
```

#### Kyle Miller (Jul 16 2021 at 23:39):

(I'm sure those with more facility than me with complex numbers and algebraic expressions could simplify the proof of the supporting lemma.)

Last updated: Dec 20 2023 at 11:08 UTC