Theorem Complex.tan_of_real_re

Modification history

2023-06-10 02:10

Mathlib/Data/Complex/Exponential.lean

chore: use `ofReal` instead of `of_real` in lemma names (#4934)

Deleted Complex.tan_of_real_re View on Github →

2023-03-15 16:55

Mathlib/Data/Complex/Exponential.lean

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

Added Complex.tan_of_real_re View on Github →