Theorem Complex.ofReal_cos_ofReal_re

Modification history

2025-01-27 13:29

Mathlib/Data/Complex/Exponential.lean

chore(Data/Complex/Exponential): split trig functions to new file (#21075) …

Modified Complex.ofReal_cos_ofReal_re View on Github →

2023-03-15 16:55

Mathlib/Data/Complex/Exponential.lean

feat: port Data.Complex.Exponential (#2785)

Added Complex.ofReal_cos_ofReal_re View on Github →