expHom — Mathlib

English

There is a homomorphism from (ℝ, +) to the unit circle given by t ↦ exp(t i).

Русский

Существует гомоморфизм от (ℝ, +) в единичную окружность по правилу t ↦ e^{i t}.

LaTeX

$$$$ \\tau: \\mathbb{R} \\to \\mathrm{Circle}, \\quad \\tau(t) = \\exp(t\,i), \\quad \\tau(x+y) = \\tau(x) \\tau(y). $$$$

Lean4

/-- The map `fun t => exp (t * I)` from `ℝ` to the unit circle in `ℂ`,
considered as a homomorphism of groups. -/
@[simps]
def expHom : ℝ →+ Additive Circle where
  toFun := Additive.ofMul ∘ exp
  map_zero' := exp_zero
  map_add' := exp_add

Похожие утверждения