Def Tactic.evalExp

Modification history

2023-07-18 03:34

Mathlib/Data/Complex/Exponential.lean

feat: `positivity` extension for `Real.log` of natural/integer casts and numeric literals (#5839) …

Deleted Tactic.evalExp View on Github →

2023-03-15 16:55

Mathlib/Data/Complex/Exponential.lean

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

Added Tactic.evalExp View on Github →