TODO

Rename

• exp_map_circle → circle.exp
• coe_inv_circle_eq_conj → circle.coe_inv_eq_conj
• coe_div_circle → circle.coe_div + norm_cast

@[simp]

theorem Circle.coe_exp (r : ℝ) : ↑(expMapCircle r) = Complex.exp (↑r * Complex.I)

theorem Circle.exp_int_mul_two_pi (n : ℤ) : expMapCircle (↑n * (2 * Real.pi)) = 1

theorem Circle.exp_two_pi_mul_int (n : ℤ) : expMapCircle (2 * Real.pi * ↑n) = 1

theorem Circle.exp_two_pi : expMapCircle (2 * Real.pi) = 1

theorem Circle.exp_eq_one {r : ℝ} : expMapCircle r = 1 ↔ ∃ (n : ℤ), r = ↑n * (2 * Real.pi)

noncomputable def Circle.e : AddChar ℝ ↥circle

Equations

• Circle.e = { toFun := fun (r : ℝ) => expMapCircle (2 * Real.pi * r), map_zero_one' := Circle.e.proof_2, map_add_mul' := Circle.e.proof_3 }

theorem Circle.e_apply (r : ℝ) : Circle.e r = expMapCircle (2 * Real.pi * r)

@[simp]

theorem Circle.coe_e (r : ℝ) : ↑(Circle.e r) = Complex.exp (↑(2 * Real.pi * r) * Complex.I)

@[simp]

theorem Circle.e_int (z : ℤ) : Circle.e ↑z = 1

@[simp]

theorem Circle.e_one : Circle.e 1 = 1

@[simp]

theorem Circle.e_add_int {r : ℝ} {z : ℤ} : Circle.e (r + ↑z) = Circle.e r

@[simp]

theorem Circle.e_sub_int {r : ℝ} {z : ℤ} : Circle.e (r - ↑z) = Circle.e r

@[simp]

theorem Circle.e_fract (r : ℝ) : Circle.e (Int.fract r) = Circle.e r

@[simp]

theorem Circle.e_mod_div {m : ℤ} {n : ℕ} : Circle.e (↑(m % ↑n) / ↑n) = Circle.e (↑m / ↑n)

theorem Circle.e_eq_one {r : ℝ} : Circle.e r = 1 ↔ ∃ (n : ℤ), r = ↑n

theorem Circle.e_inj {r : ℝ} {s : ℝ} : Circle.e r = Circle.e s ↔ r ≡ s [PMOD 1]