Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-18 13:27 fa0e7570

View on Github →

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

Estimated changes

Modified src/algebra/group.lean

added theorem add_add_sub_cancel

added theorem add_sub_sub_cancel

added theorem mul_mul_mul_comm

added theorem sub_add_add_cancel

Modified src/algebra/group_power.lean

added theorem sq_sub_sq

Modified src/algebra/ring.lean

added theorem mul_self_sub_mul_self

Modified src/analysis/complex/exponential.lean

Modified src/data/complex/basic.lean

added theorem complex.I_sq

added theorem complex.eq_conj_iff_re

modified theorem complex.eq_conj_iff_real

Modified src/data/complex/exponential.lean

added theorem complex.cos_add_sin_I

added theorem complex.cos_sub_sin_I

added theorem complex.cos_two_mul'

added theorem complex.cosh_add_sinh

added theorem complex.cosh_mul_I

added theorem complex.cosh_sq_sub_sinh_sq

added theorem complex.cosh_sub_sinh

deleted theorem complex.sin_pow_two_add_cos_pow_two

added theorem complex.sin_sq_add_cos_sq

added theorem complex.sinh_add_cosh

added theorem complex.sinh_mul_I

added theorem complex.two_cos

added theorem complex.two_cosh

added theorem complex.two_sin

added theorem complex.two_sinh

deleted theorem real.cos_pow_two_le_one

added theorem real.cos_sq_le_one

modified theorem real.exp_injective

modified theorem real.exp_le_exp

modified theorem real.exp_lt_exp

added theorem real.exp_strict_mono

deleted theorem real.sin_pow_two_add_cos_pow_two

deleted theorem real.sin_pow_two_le_one

added theorem real.sin_sq_add_cos_sq

added theorem real.sin_sq_le_one