mathlib3

fa0e7570 - refactor(data/complex/exponential): improve trig proofs (#1041)

refactor(data/complex/exponential): improve trig proofs (#1041) * fix(data/complex/exponential): make complex.exp irreducible 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. * refactor(data/complex/exponential): improve trig proofs * fix build * fix(algebra/group): prove lemma for comm_semigroup instead of comm_monoid