mathlib
a6c1f377 - fix(data/complex/exponential): make complex.exp irreducible (#1040)

Commit
6 years ago
fix(data/complex/exponential): make complex.exp irreducible (#1040) See discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/-T50000.20challenge Using `ring` (and other tactics) on terms involving `exp` can lead to some unpleasant and unnecessary unfolding.
Author
Committer
Parents
Loading