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 ℝ { x // x ∈ circle }

Equations

• One or more equations did not get rendered due to their size.

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]