Continuous one-parameter subgroups of the complex units

Every continuous homomorphism from the additive real line to ℂˣ is an exponential t ↦ exp (t * s) for a unique s : ℂ, without any differentiability hypothesis. This is the automatic-smoothness statement for the one-parameter subgroups of ℂˣ: the restriction of a continuous character of ℝˣ or ℂˣ to a one-parameter subgroup, such as the positive reals or the unit circle, is recorded by a single complex parameter.

Main results

• TauCeti.existsUnique_eq_expUnitHom_complex: continuous homomorphisms ℝ → ℂˣ are exponentials.

theorem TauCeti.existsUnique_eq_expUnitHom_complex (φ : Multiplicative ℝ →ₜ* ℂˣ) : ∃! s : ℂ, φ = expUnitHom s

Continuous homomorphisms ℝ → ℂˣ are exponentials. Every continuous homomorphism from the additive real line to ℂˣ is t ↦ exp (t * s) for a unique s : ℂ. Unlike existsUnique_eq_expUnitHom, no differentiability is assumed.