mathlib
7f256987 - feat(analysis/complex/isometry): Show that certain complex isometries are not equal (#8646)

Commit
4 years ago
feat(analysis/complex/isometry): Show that certain complex isometries are not equal (#8646) 1. Lemma `reflection_rotation` proves that rotation by `(a : circle)` is not equal to reflection over the x-axis (i.e, `conj_lie`). 2. Lemma `rotation_injective` proves that rotation by different `(a b: circle)` are not the same,(i.e, `rotation` is injective). Co-authored by Kyle Miller
Author
Parents
Loading