Commit 2021-03-28 16:13 7285fb65

View on Github →

feat(data/complex/circle): circle is a Lie group (#6907) Define circle to be the unit circle in ℂ and give it the structure of a Lie group. Also define exp_map_circle to be the natural map λ t, exp (t * I) from ℝ to circle, and give it (separately) the structures of a group homomorphism and a smooth map (we seem not to have the definition of a Lie group homomorphism).

Estimated changes

Modified src/data/complex/module.lean

added theorem complex.findim_real_complex_fact

Created src/geometry/manifold/instances/circle.lean

added theorem abs_eq_of_mem_circle

added def circle

added theorem circle_def

added theorem coe_div_circle

added theorem coe_inv_circle

added def exp_map_circle

added def exp_map_circle_hom

added theorem mem_circle_iff_abs

added theorem times_cont_mdiff_exp_map_circle