Phase exponential times conjugate is 1

Proved

KobayashiMaskawa1973.exp_I_mul_star_exp_I

by Mazecto · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysis

For any real number $t \in \mathbb{R}$ , the complex phase $e^{it}$ satisfies:

e^{it} (e^{it})^* = e^{it} e^{-it} = 1.

Preamble

import Mathlib

Formal statement

namespace KobayashiMaskawa1973

theorem exp_I_mul_star_exp_I (t : ℝ) :
    Complex.exp ((t : ℂ) * Complex.I) * star (Complex.exp ((t : ℂ) * Complex.I)) = 1 := by sorry

end KobayashiMaskawa1973

Source

Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

View graph