Trigonometric

📁 Source: Mathlib/Analysis/Complex/Trigonometric.lean

Statistics

Metric	Count
Definitions cos, cosh, cot, sin, sinh, tan, tanh, evalCosh, cos, cosh, cot, sin, sinh, tan, tanh	15
Theorems cos_add, cos_add_cos, cos_add_mul_I, cos_add_sin_I, cos_add_sin_mul_I_pow, cos_bound, cos_conj, cos_eq, cos_mul_I, cos_neg, cos_ofReal_im, cos_ofReal_re, cos_sq, cos_sq', cos_sq_add_sin_sq, cos_sub, cos_sub_cos, cos_sub_sin_I, cos_three_mul, cos_two_mul, cos_two_mul', cos_zero, cosh_add, cosh_add_sinh, cosh_conj, cosh_mul_I, cosh_neg, cosh_ofReal_im, cosh_ofReal_re, cosh_sq, cosh_sq_sub_sinh_sq, cosh_sub, cosh_sub_sinh, cosh_three_mul, cosh_two_mul, cosh_zero, cot_conj, cot_eq_cos_div_sin, cot_inv_eq_tan, enorm_exp_I_mul_ofReal, enorm_exp_ofReal_mul_I, exp_add_mul_I, exp_eq_exp_re_mul_sin_add_cos, exp_im, exp_mul_I, exp_ofReal_mul_I_im, exp_ofReal_mul_I_re, exp_re, exp_sub_cosh, exp_sub_sinh, inv_one_add_tan_sq, nnnorm_exp_I_mul_ofReal, nnnorm_exp_ofReal_mul_I, norm_cos_add_sin_mul_I, norm_exp, norm_exp_I_mul_ofReal, norm_exp_I_mul_ofReal_sub_one, norm_exp_eq_iff_re_eq, norm_exp_ofReal_mul_I, ofReal_cos, ofReal_cos_ofReal_re, ofReal_cosh, ofReal_cosh_ofReal_re, ofReal_cot, ofReal_cot_ofReal_re, ofReal_sin, ofReal_sin_ofReal_re, ofReal_sinh, ofReal_sinh_ofReal_re, ofReal_tan, ofReal_tan_ofReal_re, ofReal_tanh, ofReal_tanh_ofReal_re, one_add_tan_sq_mul_cos_sq_eq_one, sin_add, sin_add_mul_I, sin_add_sin, sin_bound, sin_conj, sin_eq, sin_mul_I, sin_neg, sin_ofReal_im, sin_ofReal_re, sin_sq, sin_sq_add_cos_sq, sin_sub, sin_sub_sin, sin_three_mul, sin_two_mul, sin_zero, sinh_add, sinh_add_cosh, sinh_conj, sinh_mul_I, sinh_neg, sinh_ofReal_im, sinh_ofReal_re, sinh_sq, sinh_sub, sinh_sub_cosh, sinh_three_mul, sinh_two_mul, sinh_zero, tan_conj, tan_eq_sin_div_cos, tan_inv_eq_cot, tan_mul_I, tan_mul_cos, tan_neg, tan_ofReal_im, tan_ofReal_re, tan_sq_div_one_add_tan_sq, tan_zero, tanh_conj, tanh_eq_sinh_div_cosh, tanh_mul_I, tanh_neg, tanh_ofReal_im, tanh_ofReal_re, tanh_zero, two_cos, two_cosh, two_sin, two_sinh, abs_cos_eq_sqrt_one_sub_sin_sq, abs_cos_le_one, abs_sin_eq_sqrt_one_sub_cos_sq, abs_sin_le_one, abs_tanh_lt_one, cos_abs, cos_add, cos_add_cos, cos_bound, cos_le_one, cos_neg, cos_one_le, cos_one_pos, cos_pos_of_le_one, cos_sq, cos_sq', cos_sq_add_sin_sq, cos_sq_le_one, cos_sub, cos_sub_cos, cos_three_mul, cos_two_mul, cos_two_mul', cos_two_neg, cos_zero, cosh_abs, cosh_add, cosh_add_sinh, cosh_eq, cosh_neg, cosh_pos, cosh_sq, cosh_sq', cosh_sq_sub_sinh_sq, cosh_sub, cosh_sub_sinh, cosh_three_mul, cosh_two_mul, cosh_zero, cot_eq_cos_div_sin, cot_inv_eq_tan, exp_sub_cosh, exp_sub_sinh, inv_one_add_tan_sq, inv_sqrt_one_add_tan_sq, neg_one_le_cos, neg_one_le_sin, neg_one_lt_tanh, one_add_tan_sq_mul_cos_sq_eq_one, sin_add, sin_add_sin, sin_bound, sin_le_one, sin_neg, sin_pos_of_pos_of_le_one, sin_pos_of_pos_of_le_two, sin_sq, sin_sq_add_cos_sq, sin_sq_eq_half_sub, sin_sq_le_one, sin_sub, sin_sub_sin, sin_three_mul, sin_two_mul, sin_zero, sinh_add, sinh_add_cosh, sinh_eq, sinh_lt_cosh, sinh_neg, sinh_sq, sinh_sub, sinh_sub_cosh, sinh_three_mul, sinh_two_mul, sinh_zero, tan_div_sqrt_one_add_tan_sq, tan_eq_sin_div_cos, tan_inv_eq_cot, tan_mul_cos, tan_neg, tan_sq_div_one_add_tan_sq, tan_zero, tanh_eq, tanh_eq_sinh_div_cosh, tanh_lt_one, tanh_neg, tanh_sq_lt_one, tanh_zero, two_mul_cos_mul_cos, two_mul_sin_mul_cos, two_mul_sin_mul_sin	217
Total	232

Complex

Definitions

Name	Category	Theorems
cos 📖	CompOp	173 math math: cos_sub_pi, Polynomial.Chebyshev.S_two_mul_complex_cos, cos_eq_tsum, EulerSine.integral_cos_mul_cos_pow, HasDerivAt.ccos, one_add_tan_sq_mul_cos_sq_eq_one, sin_eq_zero_iff_cos_eq, HasFDerivWithinAt.ccos, cos_three_mul, sin_pi_div_two_sub, HasStrictFDerivAt.csin, cos_mul_I, cos_sub_sin_I, cos_eq_one_iff, exp_add_mul_I, range_cos, cos_ofReal_re, cos_eq_zero_iff, cos_sub, cos_antiperiodic, cos_add_nat_mul_two_pi, hasStrictDerivAt_tan, deriv_cos, norm_cos_add_sin_mul_I, cos_pi_div_two, HasFDerivWithinAt.csin, continuousOn_cos, cos_conj, cos_eq_two_mul_tan_half_div_one_sub_tan_half_sq, cos_nat_mul_two_pi_sub_pi, ContDiff.ccos, EulerSine.integral_cos_mul_cos_pow_aux, HasStrictDerivAt.csin, Differentiable.ccos, arg_cos_add_sin_mul_I, cos_eq_iff_quadratic, riemannZeta_one_sub, cos_nat_mul_two_pi, sin_two_mul, ofReal_cos_ofReal_re, arg_mul_cos_add_sin_mul_I_eq_toIocMod, arg_cos_add_sin_mul_I_sub, cos_eq_tsum', cos_pi_sub, cos_two_mul, cos_sub_two_pi, sin_sub_pi_div_two, Measurable.ccos, cos_add_sin_mul_I_pow, arg_mul_cos_add_sin_mul_I, DifferentiableOn.ccos, cos_int_mul_two_pi_sub, iteratedDeriv_odd_sin, HurwitzZeta.cosZeta_one_sub, EulerSine.sin_pi_mul_eq, fderivWithin_ccos, ContDiffOn.ccos, HasDerivAt.csin, cos_add_pi, HasStrictFDerivAt.ccos, cos_add_sin_I, ContDiffWithinAt.ccos, HasFDerivAt.ccos, hasDerivAt_cos, cos_sub_nat_mul_two_pi, cos_int_mul_two_pi_add_pi, cos_two_mul', cos_surjective, EulerSine.integral_sin_mul_sin_mul_cos_pow_eq, measurable_cos, HurwitzZeta.hurwitzZetaEven_one_sub, deriv_csin, tan_mul_cos, cos_add, norm_mul_cos_add_sin_mul_I, analyticOn_cos, cos_periodic, tan_eq_sin_div_cos, cos_bound, continuousOn_tan, iteratedDeriv_even_cos, iteratedDeriv_add_one_sin, sin_sq_add_cos_sq, fderiv_ccos, cos_add_pi_div_two, hasStrictDerivAt_cos, HasDerivWithinAt.csin, iteratedDeriv_add_one_cos, continuous_cos, hasSum_cos', cos_add_cos, hasStrictDerivAt_sin, derivWithin_ccos, cos_sq_add_sin_sq, cos_sub_pi_div_two, deriv_tan, cos_zero, ContDiffAt.ccos, Polynomial.Chebyshev.T_complex_cos, cos_add_mul_I, cos_int_mul_two_pi_sub_pi, cos_add_two_pi, HasFDerivAt.csin, derivWithin_csin, hasDerivAt_sin, deriv_ccos, sin_add, HasDerivWithinAt.ccos, cos_neg, sin_eq, EulerSine.antideriv_cos_comp_const_mul, fderivWithin_csin, EulerSine.antideriv_sin_comp_const_mul, cot_eq_cos_div_sin, deriv_cos', isIntegral_two_mul_cos_rat_mul_pi, Gammaℝ_one_sub_mul_Gammaℝ_one_add, iteratedDeriv_odd_cos, ofReal_cos, sin_sub, cos_eq, Polynomial.Chebyshev.U_complex_cos, sin_add_sin, Polynomial.Chebyshev.C_two_mul_complex_cos, sin_add_mul_I, cos_pi_div_two_sub, cos_sub_cos, cos_eq_zero_iff_sin_eq, exp_eq_exp_re_mul_sin_add_cos, AEMeasurable.ccos, continuous_tan, deriv_sin, cos_sq, hasDerivAt_tan, Gammaℝ_div_Gammaℝ_one_sub, cos_eq_neg_one_iff, logDeriv_cos, differentiable_iteratedDeriv_cos, sin_sq, differentiable_cos, cos_nat_mul_two_pi_sub, analyticAt_cos, analyticOnNhd_cos, inv_one_add_tan_sq, cos_nat_mul_two_pi_add_pi, inv_Gammaℝ_one_sub, fderiv_csin, exp_mul_I, isAlgebraic_cos_rat_mul_pi, contDiff_cos, arg_mul_cos_add_sin_mul_I_sub, cos_two_pi_sub, DifferentiableAt.ccos, sin_sub_sin, hasSum_cos, cos_ofReal_im, differentiableAt_cos, cos_eq_cos_iff, cos_sq', integral_cos_mul_complex, cosh_mul_I, cos_int_mul_two_pi, cos_two_pi, cos_add_int_mul_two_pi, analyticWithinAt_cos, arg_cos_add_sin_mul_I_eq_toIocMod, DifferentiableWithinAt.ccos, EulerSine.integral_cos_mul_cos_pow_even, HasStrictDerivAt.ccos, cos_pi, cos_sub_int_mul_two_pi, sin_add_pi_div_two, two_cos
cosh 📖	CompOp	89 math math: HasFDerivWithinAt.ccosh, iteratedDeriv_even_cosh, analyticAt_cosh, cos_mul_I, fderivWithin_csinh, ContDiffOn.ccosh, ofReal_cosh_ofReal_re, deriv_csinh, iteratedDeriv_odd_sinh, cosh_conj, cosh_three_mul, analyticWithinAt_cosh, sinh_add_cosh, fderivWithin_ccosh, contDiff_cosh, analyticOn_cosh, cosh_ofReal_im, HasDerivWithinAt.csinh, cosh_sq_sub_sinh_sq, AEMeasurable.ccosh, continuous_cosh, DifferentiableAt.ccosh, HasDerivAt.csinh, hasStrictDerivAt_sinh, HasFDerivWithinAt.csinh, deriv_ccosh, HasDerivAt.ccosh, HasStrictDerivAt.csinh, Polynomial.Chebyshev.T_complex_cosh, sinh_sq, Polynomial.Chebyshev.C_two_mul_complex_cosh, hasDerivAt_sinh, tanh_eq_sinh_div_cosh, HasDerivWithinAt.ccosh, cosh_zero, cosh_sq, derivWithin_ccosh, HasFDerivAt.ccosh, cosh_eq_tsum, two_cosh, sinh_two_mul, cosh_two_mul, ContDiff.ccosh, cosh_sub, ContDiffAt.ccosh, iteratedDeriv_add_one_sinh, sinh_add, ContDiffWithinAt.ccosh, deriv_cosh, Polynomial.Chebyshev.U_complex_cosh, analyticOnNhd_cosh, DifferentiableWithinAt.ccosh, hasDerivAt_cosh, cos_add_mul_I, exp_sub_cosh, hasStrictDerivAt_cosh, Polynomial.Chebyshev.S_two_mul_complex_cosh, sin_eq, differentiableAt_cosh, exp_sub_sinh, Measurable.ccosh, cos_eq, fderiv_ccosh, DifferentiableOn.ccosh, sin_add_mul_I, HasStrictDerivAt.ccosh, measurable_cosh, cosh_add, iteratedDeriv_add_one_cosh, cosh_neg, deriv_sinh, derivWithin_csinh, fderiv_csinh, HasFDerivAt.csinh, differentiable_cosh, sinh_sub, ofReal_cosh, HasStrictFDerivAt.ccosh, iteratedDeriv_odd_cosh, hasSum_cosh, cosh_ofReal_re, HasStrictFDerivAt.csinh, cosh_mul_I, sinh_sub_cosh, Differentiable.ccosh, cosh_sub_sinh, logDeriv_cosh, cosh_add_sinh, differentiable_iteratedDeriv_cosh
cot 📖	CompOp	18 math math: cot_inv_eq_tan, ofReal_cot, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow, cot_series_rep', logDeriv_sin_div_eq_cot, logDeriv_sin, ofReal_cot_ofReal_re, cot_pi_eq_exp_ratio, cot_series_rep, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow, cot_conj, cot_pi_mul_contDiffWithinAt, tendsto_logDeriv_euler_cot_sub, cot_eq_cos_div_sin, iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum, cot_eq_exp_ratio, tan_inv_eq_cot, pi_mul_cot_pi_q_exp
sin 📖	CompOp	161 math math: AEMeasurable.csin, Polynomial.Chebyshev.S_two_mul_complex_cos, ContDiffAt.csin, HasDerivAt.ccos, differentiableAt_sin, Measurable.csin, Differentiable.csin, sin_eq_zero_iff_cos_eq, HasFDerivWithinAt.ccos, sin_pi_div_two_sub, HasStrictFDerivAt.csin, cos_sub_sin_I, exp_add_mul_I, analyticOn_sin, cos_sub, HasProdUniformlyOn_sineTerm_prod_on_compact, sin_eq_neg_one_iff, range_sin, continuous_sin, sin_int_mul_pi, sin_eq_zero_iff, ofReal_sin_ofReal_re, deriv_cos, norm_cos_add_sin_mul_I, HasFDerivWithinAt.csin, sin_nat_mul_pi, sin_int_mul_two_pi_sub, sin_bound, EulerSine.integral_cos_mul_cos_pow_aux, HasStrictDerivAt.csin, arg_cos_add_sin_mul_I, sin_sub_nat_mul_two_pi, sin_nat_mul_two_pi_sub, sin_two_mul, analyticAt_sin, arg_mul_cos_add_sin_mul_I_eq_toIocMod, arg_cos_add_sin_mul_I_sub, sin_sub_two_pi, sin_sub_pi_div_two, cos_add_sin_mul_I_pow, arg_mul_cos_add_sin_mul_I, ContDiffOn.csin, continuousOn_sin, differentiable_iteratedDeriv_sin, iteratedDeriv_odd_sin, tendsto_logDeriv_euler_sin_div, logDeriv_sin_div_eq_cot, EulerSine.sin_pi_mul_eq, logDeriv_sin, fderivWithin_ccos, isAlgebraic_sin_rat_mul_pi, HasDerivAt.csin, sin_two_pi, HasStrictFDerivAt.ccos, analyticOnNhd_sin, hasSum_sin, sin_add_two_pi, cos_add_sin_I, sin_eq_sin_iff, HasProdLocallyUniformlyOn_euler_sin_prod, sin_pi_sub, HasFDerivAt.ccos, sin_three_mul, hasDerivAt_cos, cos_two_mul', tendsto_euler_sin_prod, EulerSine.integral_sin_mul_sin_mul_cos_pow_eq, sin_conj, isIntegral_two_mul_sin_rat_mul_pi, deriv_csin, DifferentiableWithinAt.csin, tan_mul_cos, sin_antiperiodic, cos_add, norm_mul_cos_add_sin_mul_I, differentiable_sin, sin_eq_one_iff, tan_eq_sin_div_cos, iteratedDeriv_add_one_sin, sin_sq_add_cos_sq, sin_ofReal_re, fderiv_ccos, cos_add_pi_div_two, hasStrictDerivAt_cos, HasDerivWithinAt.csin, iteratedDeriv_add_one_cos, hasStrictDerivAt_sin, derivWithin_ccos, cos_sq_add_sin_sq, sin_pi_div_two, sin_periodic, cos_sub_pi_div_two, ContDiffWithinAt.csin, cos_add_mul_I, HasFDerivAt.csin, derivWithin_csin, hasDerivAt_sin, deriv_ccos, sin_add, HasDerivWithinAt.ccos, sin_eq, EulerSine.antideriv_cos_comp_const_mul, sin_eq_two_mul_tan_half_div_one_add_tan_half_sq, fderivWithin_csin, sin_add_int_mul_two_pi, EulerSine.antideriv_sin_comp_const_mul, cot_eq_cos_div_sin, deriv_cos', sin_pi, sin_eq_tsum, measurable_sin, euler_sineTerm_tprod, iteratedDeriv_odd_cos, sin_sub, cos_eq, Polynomial.Chebyshev.U_complex_cos, sin_add_sin, sin_mul_I, sin_sub_pi, sin_add_mul_I, iteratedDeriv_even_sin, cos_pi_div_two_sub, cos_sub_cos, cos_eq_zero_iff_sin_eq, exp_eq_exp_re_mul_sin_add_cos, ofReal_sin, sin_neg, sin_sub_int_mul_two_pi, sin_two_pi_sub, sin_ofReal_im, deriv_sin, analyticWithinAt_sin, tan_sq_div_one_add_tan_sq, sin_zero, hasSum_sin', Gamma_mul_Gamma_one_sub, sin_eq_tsum', sin_surjective, sin_sq, fderiv_csin, exp_mul_I, contDiff_sin, arg_mul_cos_add_sin_mul_I_sub, tendsto_euler_sin_prod', sin_sub_sin, HurwitzZeta.hurwitzZetaOdd_one_sub, sinh_mul_I, sin_add_nat_mul_two_pi, ContDiff.csin, cos_sq', DifferentiableOn.csin, integral_cos_mul_complex, HurwitzZeta.sinZeta_one_sub, inv_Gammaℝ_two_sub, arg_cos_add_sin_mul_I_eq_toIocMod, HasStrictDerivAt.ccos, DifferentiableAt.csin, isEquivalent_sin, sin_add_pi, two_sin, sin_add_pi_div_two
sinh 📖	CompOp	87 math math: HasFDerivWithinAt.ccosh, sinh_conj, fderivWithin_csinh, deriv_csinh, DifferentiableAt.csinh, iteratedDeriv_odd_sinh, AEMeasurable.csinh, sinh_add_cosh, fderivWithin_ccosh, two_sinh, analyticOn_sinh, DifferentiableOn.csinh, sinh_three_mul, HasDerivWithinAt.csinh, cosh_sq_sub_sinh_sq, HasDerivAt.csinh, hasStrictDerivAt_sinh, HasFDerivWithinAt.csinh, ofReal_sinh_ofReal_re, deriv_ccosh, sinh_zero, HasDerivAt.ccosh, continuous_sinh, HasStrictDerivAt.csinh, sinh_sq, hasDerivAt_sinh, sinh_neg, isEquivalent_sinh, tanh_eq_sinh_div_cosh, Measurable.csinh, HasDerivWithinAt.ccosh, cosh_sq, derivWithin_ccosh, HasFDerivAt.ccosh, sinh_two_mul, cosh_two_mul, cosh_sub, sinh_ofReal_re, iteratedDeriv_add_one_sinh, sinh_add, DifferentiableWithinAt.csinh, analyticAt_sinh, deriv_cosh, Polynomial.Chebyshev.U_complex_cosh, analyticWithinAt_sinh, hasDerivAt_cosh, contDiff_sinh, cos_add_mul_I, exp_sub_cosh, Differentiable.csinh, hasStrictDerivAt_cosh, measurable_sinh, Polynomial.Chebyshev.S_two_mul_complex_cosh, sin_eq, sinh_ofReal_im, sinh_eq_tsum, ofReal_sinh, exp_sub_sinh, cos_eq, fderiv_ccosh, sin_mul_I, sin_add_mul_I, HasStrictDerivAt.ccosh, cosh_add, differentiable_sinh, iteratedDeriv_even_sinh, differentiable_iteratedDeriv_sinh, differentiableAt_sinh, ContDiffAt.csinh, iteratedDeriv_add_one_cosh, ContDiff.csinh, deriv_sinh, derivWithin_csinh, hasSum_sinh, fderiv_csinh, ContDiffWithinAt.csinh, HasFDerivAt.csinh, sinh_sub, HasStrictFDerivAt.ccosh, iteratedDeriv_odd_cosh, sinh_mul_I, HasStrictFDerivAt.csinh, ContDiffOn.csinh, analyticOnNhd_sinh, sinh_sub_cosh, cosh_sub_sinh, cosh_add_sinh
tan 📖	CompOp	57 math math: one_add_tan_sq_mul_cos_sq_eq_one, tan_add_mul_I, tan_nat_mul_pi_sub, tan_pi_sub, hasStrictDerivAt_tan, tan_pi_div_two_sub, tan_int_mul_pi, tan_eq, cot_inv_eq_tan, cos_eq_two_mul_tan_half_div_one_sub_tan_half_sq, tan_nat_mul_pi, tan_eq_zero_of_cos_eq_zero, tan_eq_zero_iff', tan_ofReal_re, tan_neg, tan_int_mul_pi_div_two, tan_ofReal_im, tan_sub', tan_add, tendsto_norm_tan_atTop, tan_add', tan_sub_int_mul_pi, differentiableAt_tan, tan_sub, tan_zero, arctan_tan, tan_mul_cos, tan_sub_nat_mul_pi, tan_eq_sin_div_cos, tan_sub_pi, tan_add_pi, continuousOn_tan, ofReal_tan_ofReal_re, contDiffAt_tan, deriv_tan, tan_int_mul_pi_sub, tendsto_norm_tan_of_cos_eq_zero, tanh_mul_I, tan_arctan, sin_eq_two_mul_tan_half_div_one_add_tan_half_sq, tan_add_int_mul_pi, tan_add_nat_mul_pi, tan_eq_zero_iff, continuous_tan, hasDerivAt_tan, tan_sq_div_one_add_tan_sq, isAlgebraic_tan_rat_mul_pi, logDeriv_cos, tan_mul_I, inv_one_add_tan_sq, tan_conj, tan_periodic, tan_inv_eq_cot, continuousAt_tan, tan_two_mul, tan_eq_one_sub_tan_half_sq_div_one_add_tan_half_sq, ofReal_tan
tanh 📖	CompOp	13 math math: tan_add_mul_I, tan_eq, ofReal_tanh, tanh_neg, tanh_eq_sinh_div_cosh, tanh_conj, tanh_ofReal_re, tanh_ofReal_im, tanh_mul_I, tanh_zero, tan_mul_I, logDeriv_cosh, ofReal_tanh_ofReal_re

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cos_add 📖	mathematical	—	cos Complex instAdd instSub instMul sin	—	cosh_mul_I add_mul Distrib.rightDistribClass cosh_add sinh_mul_I mul_mul_mul_comm I_mul_I mul_neg_one sub_eq_add_neg
cos_add_cos 📖	mathematical	—	Complex instAdd cos instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv instDivInvMonoid instSub	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Meta.NormNum.isNat_eq_false instCharZero Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt cos_add cos_sub Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one
cos_add_mul_I 📖	mathematical	—	cos Complex instAdd instMul I instSub cosh sin sinh	—	cos_add cos_mul_I sin_mul_I mul_assoc
cos_add_sin_I 📖	mathematical	—	Complex instAdd cos instMul sin I exp	—	cosh_add_sinh sinh_mul_I cosh_mul_I
cos_add_sin_mul_I_pow 📖	mathematical	—	Complex Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instAdd cos instMul sin I instNatCast	—	exp_mul_I exp_nat_mul mul_assoc
cos_bound 📖	mathematical	Real Real.instLE Norm.norm Complex instNorm Real.instOne	instSub cos instOne DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat Real.instMul Real.instMonoid Real.instDivInvMonoid Real.instNatCast	—	Nat.instAtLeastTwoHAddOfNat neg_mul Finset.sum_congr Finset.sum_range_succ Finset.sum_singleton pow_zero Nat.cast_one div_self NeZero.charZero_one instCharZero pow_one zero_add mul_one div_one Even.neg_pow Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one one_ne_zero NeZero.one GroupWithZero.toNontrivial le_imp_le_of_le_of_le norm_add_le le_refl norm_div norm_ofNat add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing exp_bound norm_neg norm_mul norm_I IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo add_le_add_right Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_natSucc Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_factorial Mathlib.Meta.NormNum.isNNRat_div add_halves CharZero.NeZero.two
cos_conj 📖	mathematical	—	cos DFunLike.coe RingHom Complex Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	cosh_mul_I conj_neg_I map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass cosh_conj mul_neg cosh_neg
cos_eq 📖	mathematical	—	cos Complex instSub instMul ofReal re cosh im sin sinh I	—	re_add_im cos_add_mul_I
cos_mul_I 📖	mathematical	—	cos Complex instMul I cosh	—	cosh_mul_I Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero I_sq mul_neg cosh_neg
cos_neg 📖	mathematical	—	cos Complex instNeg	—	neg_mul exp_neg neg_neg add_comm
cos_ofReal_im 📖	mathematical	—	im cos ofReal Real Real.instZero	—	ofReal_cos_ofReal_re ofReal_im
cos_ofReal_re 📖	mathematical	—	re cos ofReal Real.cos	—	—
cos_sq 📖	mathematical	—	Complex Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring cos instAdd DivInvMonoid.toDiv instDivInvMonoid instOne instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instMul	—	Nat.instAtLeastTwoHAddOfNat cos_two_mul add_sub_cancel mul_div_cancel_left₀ GroupWithZero.toMulDivCancelClass instCharZero
cos_sq' 📖	mathematical	—	Complex Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring cos instSub instOne sin	—	sin_sq_add_cos_sq add_sub_cancel_left
cos_sq_add_sin_sq 📖	mathematical	—	Complex instAdd Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring cos sin instOne	—	add_comm sin_sq_add_cos_sq
cos_sub 📖	mathematical	—	cos Complex instSub instAdd instMul sin	—	sub_eq_add_neg cos_add cos_neg sin_neg mul_neg neg_neg
cos_sub_cos 📖	mathematical	—	Complex instSub cos instMul instNeg instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat sin DivInvMonoid.toDiv instDivInvMonoid instAdd	—	Nat.instAtLeastTwoHAddOfNat cos_add cos_sub add_self_div_two CharZero.NeZero.two instCharZero add_sub_cancel_right add_right_comm add_sub add_div add_sub_cancel_left sub_add div_sub_div_same Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one
cos_sub_sin_I 📖	mathematical	—	Complex instSub cos instMul sin I exp instNeg	—	neg_mul cosh_sub_sinh sinh_mul_I cosh_mul_I
cos_three_mul 📖	mathematical	—	cos Complex instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instSub Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add cos_add cos_two_mul sq mul_sub mul_one sin_two_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pp_pf_overlap cos_sq' Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Nat.cast_one Mathlib.Meta.NormNum.isInt_add
cos_two_mul 📖	mathematical	—	cos Complex instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instSub Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instOne	—	Nat.instAtLeastTwoHAddOfNat cos_two_mul' eq_sub_iff_add_eq sin_sq_add_cos_sq sub_add sub_add_eq_add_sub two_mul
cos_two_mul' 📖	mathematical	—	cos Complex instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instSub Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring sin	—	Nat.instAtLeastTwoHAddOfNat two_mul cos_add sq
cos_zero 📖	mathematical	—	cos Complex instZero instOne	—	MulZeroClass.zero_mul exp_zero neg_zero add_self_div_two CharZero.NeZero.two instCharZero
cosh_add 📖	mathematical	—	cosh Complex instAdd instMul sinh	—	Nat.instAtLeastTwoHAddOfNat mul_right_inj' IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero Field.isDomain two_ne_zero' CharZero.NeZero.two instCharZero two_cosh exp_add neg_add mul_add Distrib.leftDistribClass mul_assoc two_sinh mul_left_comm
cosh_add_sinh 📖	mathematical	—	Complex instAdd cosh sinh exp	—	Nat.instAtLeastTwoHAddOfNat mul_right_inj' IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero Field.isDomain two_ne_zero' CharZero.NeZero.two instCharZero mul_add Distrib.leftDistribClass two_cosh two_sinh add_add_sub_cancel two_mul
cosh_conj 📖	mathematical	—	cosh DFunLike.coe RingHom Complex Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	cosh.eq_1 map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass instCharZero SemilinearMapClass.distribMulActionSemiHomClass RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass exp_conj map_add SemilinearMapClass.toAddHomClass map_div₀ RingHomClass.toMonoidWithZeroHomClass map_ofNat
cosh_mul_I 📖	mathematical	—	cosh Complex instMul I cos	—	Nat.instAtLeastTwoHAddOfNat mul_right_inj' IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero Field.isDomain two_ne_zero' CharZero.NeZero.two instCharZero two_cosh two_cos neg_mul_eq_neg_mul
cosh_neg 📖	mathematical	—	cosh Complex instNeg	—	exp_neg neg_neg add_comm
cosh_ofReal_im 📖	mathematical	—	im cosh ofReal Real Real.instZero	—	ofReal_cosh_ofReal_re ofReal_im
cosh_ofReal_re 📖	mathematical	—	re cosh ofReal Real.cosh	—	—
cosh_sq 📖	mathematical	—	Complex Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring cosh instAdd sinh instOne	—	cosh_sq_sub_sinh_sq Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
cosh_sq_sub_sinh_sq 📖	mathematical	—	Complex instSub Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring cosh sinh instOne	—	sq_sub_sq cosh_add_sinh cosh_sub_sinh exp_add add_neg_cancel exp_zero
cosh_sub 📖	mathematical	—	cosh Complex instSub instMul sinh	—	sub_eq_add_neg cosh_add cosh_neg sinh_neg mul_neg
cosh_sub_sinh 📖	mathematical	—	Complex instSub cosh sinh exp instNeg	—	Nat.instAtLeastTwoHAddOfNat mul_right_inj' IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero Field.isDomain two_ne_zero' CharZero.NeZero.two instCharZero mul_sub two_cosh two_sinh add_sub_sub_cancel two_mul
cosh_three_mul 📖	mathematical	—	cosh Complex instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instSub Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add cosh_add cosh_two_mul sinh_two_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero sinh_sq Mathlib.Tactic.Ring.sub_congr Nat.cast_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.neg_mul
cosh_two_mul 📖	mathematical	—	cosh Complex instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instAdd Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring sinh	—	Nat.instAtLeastTwoHAddOfNat two_mul cosh_add sq
cosh_zero 📖	mathematical	—	cosh Complex instZero instOne	—	exp_zero neg_zero add_self_div_two CharZero.NeZero.two instCharZero
cot_conj 📖	mathematical	—	cot DFunLike.coe RingHom Complex Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	cot.eq_1 sin_conj cos_conj map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
cot_eq_cos_div_sin 📖	mathematical	—	cot Complex DivInvMonoid.toDiv instDivInvMonoid cos sin	—	—
cot_inv_eq_tan 📖	mathematical	—	Complex instInv cot tan	—	inv_div
enorm_exp_I_mul_ofReal 📖	mathematical	—	ENorm.enorm Complex NNNorm.toENorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup exp instMul I ofReal ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	toReal_enorm norm_exp_I_mul_ofReal
enorm_exp_ofReal_mul_I 📖	mathematical	—	ENorm.enorm Complex NNNorm.toENorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup exp instMul ofReal I ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	toReal_enorm norm_exp_ofReal_mul_I
exp_add_mul_I 📖	mathematical	—	exp Complex instAdd instMul I cos sin	—	exp_add exp_mul_I
exp_eq_exp_re_mul_sin_add_cos 📖	mathematical	—	exp Complex instMul ofReal re instAdd cos im sin I	—	exp_add_mul_I re_add_im
exp_im 📖	mathematical	—	im exp Real Real.instMul Real.exp re Real.sin	—	exp_eq_exp_re_mul_sin_add_cos cos_ofReal_im mul_one sin_ofReal_im MulZeroClass.mul_zero add_zero zero_add exp_ofReal_im sub_self MulZeroClass.zero_mul
exp_mul_I 📖	mathematical	—	exp Complex instMul I instAdd cos sin	—	cos_add_sin_I
exp_ofReal_mul_I_im 📖	mathematical	—	im exp Complex instMul ofReal I Real.sin	—	exp_mul_I cos_ofReal_im mul_one sin_ofReal_im MulZeroClass.mul_zero add_zero zero_add
exp_ofReal_mul_I_re 📖	mathematical	—	re exp Complex instMul ofReal I Real.cos	—	exp_mul_I MulZeroClass.mul_zero sin_ofReal_im mul_one sub_self add_zero
exp_re 📖	mathematical	—	re exp Real Real.instMul Real.exp Real.cos im	—	exp_eq_exp_re_mul_sin_add_cos MulZeroClass.mul_zero sin_ofReal_im mul_one sub_self add_zero exp_ofReal_im cos_ofReal_im zero_add MulZeroClass.zero_mul sub_zero
exp_sub_cosh 📖	mathematical	—	Complex instSub exp cosh sinh	—	sub_eq_iff_eq_add sinh_add_cosh
exp_sub_sinh 📖	mathematical	—	Complex instSub exp sinh cosh	—	sub_eq_iff_eq_add cosh_add_sinh
inv_one_add_tan_sq 📖	mathematical	—	Complex instInv instAdd instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring tan cos	—	tan_eq_sin_div_cos div_pow Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one cos_sq_add_sin_sq NeZero.charZero_one instCharZero Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial
nnnorm_exp_I_mul_ofReal 📖	mathematical	—	NNNorm.nnnorm Complex SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup exp instMul I ofReal NNReal instOneNNReal	—	nnnorm_norm norm_exp_I_mul_ofReal NNReal.coe_eq_one abs_one Real.instIsOrderedRing
nnnorm_exp_ofReal_mul_I 📖	mathematical	—	NNNorm.nnnorm Complex SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup exp instMul ofReal I NNReal instOneNNReal	—	nnnorm_norm norm_exp_ofReal_mul_I NNReal.coe_eq_one abs_one Real.instIsOrderedRing
norm_cos_add_sin_mul_I 📖	mathematical	—	Norm.norm Complex instNorm instAdd cos ofReal instMul sin I Real Real.instOne	—	Real.sin_sq_add_cos_sq MulZeroClass.mul_zero sin_ofReal_im mul_one sub_self add_comm zero_add cos_ofReal_im sq Real.sqrt_one
norm_exp 📖	mathematical	—	Norm.norm Complex instNorm exp Real.exp re	—	exp_eq_exp_re_mul_sin_add_cos norm_mul norm_exp_ofReal norm_cos_add_sin_mul_I mul_one
norm_exp_I_mul_ofReal 📖	mathematical	—	Norm.norm Complex instNorm exp instMul I ofReal Real Real.instOne	—	mul_comm norm_exp_ofReal_mul_I
norm_exp_I_mul_ofReal_sub_one 📖	mathematical	—	Norm.norm Complex instNorm instSub exp instMul I ofReal instOne Real Real.norm Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.sin DivInvMonoid.toDiv Real.instDivInvMonoid	—	Nat.instAtLeastTwoHAddOfNat norm_real two_sin one_mul exp_zero neg_add_cancel exp_add mul_assoc mul_sub add_mul Distrib.rightDistribClass Nat.cast_one add_neg_cancel ofReal_zero MulZeroClass.zero_mul add_halves CharZero.NeZero.two IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing neg_mul norm_mul norm_I mul_one neg_div' norm_exp_ofReal_mul_I norm_neg neg_sub mul_comm
norm_exp_eq_iff_re_eq 📖	mathematical	—	Norm.norm Complex instNorm exp re	—	norm_exp Real.exp_eq_exp
norm_exp_ofReal_mul_I 📖	mathematical	—	Norm.norm Complex instNorm exp instMul ofReal I Real Real.instOne	—	exp_mul_I norm_cos_add_sin_mul_I
ofReal_cos 📖	mathematical	—	ofReal Real.cos cos	—	ofReal_cos_ofReal_re
ofReal_cos_ofReal_re 📖	mathematical	—	ofReal re cos	—	conj_eq_iff_re cos_conj conj_ofReal
ofReal_cosh 📖	mathematical	—	ofReal Real.cosh cosh	—	ofReal_cosh_ofReal_re
ofReal_cosh_ofReal_re 📖	mathematical	—	ofReal re cosh	—	conj_eq_iff_re cosh_conj conj_ofReal
ofReal_cot 📖	mathematical	—	ofReal Real.cot cot	—	ofReal_cot_ofReal_re
ofReal_cot_ofReal_re 📖	mathematical	—	ofReal re cot	—	conj_eq_iff_re cot_conj conj_ofReal
ofReal_sin 📖	mathematical	—	ofReal Real.sin sin	—	ofReal_sin_ofReal_re
ofReal_sin_ofReal_re 📖	mathematical	—	ofReal re sin	—	conj_eq_iff_re sin_conj conj_ofReal
ofReal_sinh 📖	mathematical	—	ofReal Real.sinh sinh	—	ofReal_sinh_ofReal_re
ofReal_sinh_ofReal_re 📖	mathematical	—	ofReal re sinh	—	conj_eq_iff_re sinh_conj conj_ofReal
ofReal_tan 📖	mathematical	—	ofReal Real.tan tan	—	ofReal_tan_ofReal_re
ofReal_tan_ofReal_re 📖	mathematical	—	ofReal re tan	—	conj_eq_iff_re tan_conj conj_ofReal
ofReal_tanh 📖	mathematical	—	ofReal Real.tanh tanh	—	ofReal_tanh_ofReal_re
ofReal_tanh_ofReal_re 📖	mathematical	—	ofReal re tanh	—	conj_eq_iff_re tanh_conj conj_ofReal
one_add_tan_sq_mul_cos_sq_eq_one 📖	mathematical	—	Complex instMul instAdd instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring tan cos	—	sin_sq_add_cos_sq tan_mul_cos Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_gt
sin_add 📖	mathematical	—	sin Complex instAdd instMul cos	—	mul_left_inj' IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Field.isDomain I_ne_zero sinh_mul_I add_mul Distrib.rightDistribClass mul_right_comm mul_assoc cosh_mul_I sinh_add
sin_add_mul_I 📖	mathematical	—	sin Complex instAdd instMul I cosh cos sinh	—	sin_add cos_mul_I sin_mul_I mul_assoc
sin_add_sin 📖	mathematical	—	Complex instAdd sin instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv instDivInvMonoid cos instSub	—	Nat.instAtLeastTwoHAddOfNat sin_neg sub_neg_eq_add sin_sub_sin
sin_bound 📖	mathematical	Real Real.instLE Norm.norm Complex instNorm Real.instOne	instSub sin DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat Real.instMul Real.instMonoid Real.instDivInvMonoid Real.instNatCast	—	Nat.instAtLeastTwoHAddOfNat neg_mul Finset.sum_congr Finset.sum_range_succ Finset.sum_singleton pow_zero Nat.cast_one div_self NeZero.charZero_one instCharZero pow_one zero_add mul_one div_one Even.neg_pow Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one one_ne_zero NeZero.one GroupWithZero.toNontrivial le_imp_le_of_le_of_le norm_sub_le le_refl norm_div norm_mul norm_I norm_ofNat add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing exp_bound norm_neg IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo add_le_add_right Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_natSucc Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_factorial Mathlib.Meta.NormNum.isNNRat_div add_halves CharZero.NeZero.two
sin_conj 📖	mathematical	—	sin DFunLike.coe RingHom Complex Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	mul_left_inj' IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Field.isDomain I_ne_zero sinh_mul_I conj_neg_I map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass sinh_conj mul_neg sinh_neg
sin_eq 📖	mathematical	—	sin Complex instAdd instMul ofReal re cosh im cos sinh I	—	re_add_im sin_add_mul_I
sin_mul_I 📖	mathematical	—	sin Complex instMul I sinh	—	mul_comm sinh_mul_I Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero I_sq mul_neg sinh_neg neg_neg ext neg_mul MulZeroClass.zero_mul one_mul zero_sub MulZeroClass.mul_zero zero_add
sin_neg 📖	mathematical	—	sin Complex instNeg	—	neg_neg neg_mul exp_neg sub_eq_add_neg add_mul Distrib.rightDistribClass neg_div neg_add_rev
sin_ofReal_im 📖	mathematical	—	im sin ofReal Real Real.instZero	—	ofReal_sin_ofReal_re ofReal_im
sin_ofReal_re 📖	mathematical	—	re sin ofReal Real.sin	—	—
sin_sq 📖	mathematical	—	Complex Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring sin instSub instOne cos	—	sin_sq_add_cos_sq add_sub_cancel_right
sin_sq_add_cos_sq 📖	mathematical	—	Complex instAdd Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring sin cos instOne	—	cosh_mul_I sinh_mul_I mul_pow I_sq mul_neg_one sub_neg_eq_add add_comm cosh_sq_sub_sinh_sq
sin_sub 📖	mathematical	—	sin Complex instSub instMul cos	—	sub_eq_add_neg sin_add cos_neg sin_neg mul_neg
sin_sub_sin 📖	mathematical	—	Complex instSub sin instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv instDivInvMonoid cos instAdd	—	Nat.instAtLeastTwoHAddOfNat sin_add sin_sub add_self_div_two CharZero.NeZero.two instCharZero add_sub_cancel_right add_right_comm add_sub add_div add_sub_cancel_left sub_add div_sub_div_same Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one
sin_three_mul 📖	mathematical	—	sin Complex instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instSub Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add sin_add cos_two_mul cos_sq' sin_two_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.sub_congr Nat.cast_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
sin_two_mul 📖	mathematical	—	sin Complex instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat cos	—	Nat.instAtLeastTwoHAddOfNat two_mul sin_add add_mul Distrib.rightDistribClass mul_comm
sin_zero 📖	mathematical	—	sin Complex instZero	—	neg_zero MulZeroClass.zero_mul exp_zero sub_self zero_div
sinh_add 📖	mathematical	—	sinh Complex instAdd instMul cosh	—	Nat.instAtLeastTwoHAddOfNat mul_right_inj' IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero Field.isDomain two_ne_zero' CharZero.NeZero.two instCharZero two_sinh exp_add neg_add mul_add Distrib.leftDistribClass mul_assoc mul_left_comm two_cosh
sinh_add_cosh 📖	mathematical	—	Complex instAdd sinh cosh exp	—	add_comm cosh_add_sinh
sinh_conj 📖	mathematical	—	sinh DFunLike.coe RingHom Complex Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	sinh.eq_1 map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass instCharZero SemilinearMapClass.distribMulActionSemiHomClass RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass exp_conj map_sub map_div₀ RingHomClass.toMonoidWithZeroHomClass map_ofNat
sinh_mul_I 📖	mathematical	—	sinh Complex instMul I sin	—	Nat.instAtLeastTwoHAddOfNat mul_right_inj' IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero Field.isDomain two_ne_zero' CharZero.NeZero.two instCharZero two_sinh mul_assoc two_sin I_mul_I mul_neg_one neg_sub neg_mul_eq_neg_mul
sinh_neg 📖	mathematical	—	sinh Complex instNeg	—	exp_neg neg_neg neg_div neg_sub
sinh_ofReal_im 📖	mathematical	—	im sinh ofReal Real Real.instZero	—	ofReal_sinh_ofReal_re ofReal_im
sinh_ofReal_re 📖	mathematical	—	re sinh ofReal Real.sinh	—	—
sinh_sq 📖	mathematical	—	Complex Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring sinh instSub cosh instOne	—	cosh_sq_sub_sinh_sq Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add
sinh_sub 📖	mathematical	—	sinh Complex instSub instMul cosh	—	sub_eq_add_neg sinh_add cosh_neg sinh_neg mul_neg
sinh_sub_cosh 📖	mathematical	—	Complex instSub sinh cosh instNeg exp	—	neg_sub cosh_sub_sinh
sinh_three_mul 📖	mathematical	—	sinh Complex instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instAdd Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add sinh_add cosh_two_mul sinh_two_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero cosh_sq Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt
sinh_two_mul 📖	mathematical	—	sinh Complex instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat cosh	—	Nat.instAtLeastTwoHAddOfNat two_mul sinh_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one
sinh_zero 📖	mathematical	—	sinh Complex instZero	—	exp_zero neg_zero sub_self zero_div
tan_conj 📖	mathematical	—	tan DFunLike.coe RingHom Complex Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	tan.eq_1 sin_conj cos_conj map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
tan_eq_sin_div_cos 📖	mathematical	—	tan Complex DivInvMonoid.toDiv instDivInvMonoid sin cos	—	—
tan_inv_eq_cot 📖	mathematical	—	Complex instInv tan cot	—	inv_div
tan_mul_I 📖	mathematical	—	tan Complex instMul I tanh	—	tan.eq_1 sin_mul_I cos_mul_I mul_div_right_comm tanh_eq_sinh_div_cosh
tan_mul_cos 📖	mathematical	—	Complex instMul tan cos sin	—	tan_eq_sin_div_cos div_mul_cancel₀
tan_neg 📖	mathematical	—	tan Complex instNeg	—	sin_neg cos_neg neg_div
tan_ofReal_im 📖	mathematical	—	im tan ofReal Real Real.instZero	—	ofReal_tan_ofReal_re ofReal_im
tan_ofReal_re 📖	mathematical	—	re tan ofReal Real.tan	—	—
tan_sq_div_one_add_tan_sq 📖	mathematical	—	Complex DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring tan instAdd instOne sin	—	div_eq_mul_inv tan_mul_cos mul_pow inv_one_add_tan_sq
tan_zero 📖	mathematical	—	tan Complex instZero	—	sin_zero cos_zero div_one
tanh_conj 📖	mathematical	—	tanh DFunLike.coe RingHom Complex Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	tanh.eq_1 sinh_conj cosh_conj map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
tanh_eq_sinh_div_cosh 📖	mathematical	—	tanh Complex DivInvMonoid.toDiv instDivInvMonoid sinh cosh	—	—
tanh_mul_I 📖	mathematical	—	tanh Complex instMul I tan	—	tanh_eq_sinh_div_cosh cosh_mul_I sinh_mul_I mul_div_right_comm tan.eq_1
tanh_neg 📖	mathematical	—	tanh Complex instNeg	—	sinh_neg cosh_neg neg_div
tanh_ofReal_im 📖	mathematical	—	im tanh ofReal Real Real.instZero	—	ofReal_tanh_ofReal_re ofReal_im
tanh_ofReal_re 📖	mathematical	—	re tanh ofReal Real.tanh	—	—
tanh_zero 📖	mathematical	—	tanh Complex instZero	—	sinh_zero cosh_zero div_one
two_cos 📖	mathematical	—	Complex instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat cos instAdd exp I instNeg	—	mul_div_cancel₀ Nat.instAtLeastTwoHAddOfNat two_ne_zero CharZero.NeZero.two instCharZero
two_cosh 📖	mathematical	—	Complex instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat cosh instAdd exp instNeg	—	mul_div_cancel₀ Nat.instAtLeastTwoHAddOfNat two_ne_zero CharZero.NeZero.two instCharZero
two_sin 📖	mathematical	—	Complex instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat sin instSub exp instNeg I	—	mul_div_cancel₀ Nat.instAtLeastTwoHAddOfNat two_ne_zero CharZero.NeZero.two instCharZero
two_sinh 📖	mathematical	—	Complex instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat sinh instSub exp instNeg	—	mul_div_cancel₀ Nat.instAtLeastTwoHAddOfNat two_ne_zero CharZero.NeZero.two instCharZero

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
evalCosh 📖	CompOp	—

Real

Definitions

Name	Category	Theorems
cos 📖	CompOp	318 math math: cos_add_nat_mul_pi, InnerProductGeometry.cos_angle_add_of_inner_eq_zero, Polynomial.Chebyshev.isExtrOn_T_real_iff, cos_pi_div_five, iteratedDerivWithin_cos_Ioo, EulerSine.integral_cos_mul_cos_pow, sin_add_sin, ContDiffOn.cos, sin_eq_zero_iff_cos_eq, integral_cos, iteratedDeriv_odd_cos, cos_add_pi, HurwitzZeta.LSeriesHasSum_cos, analyticOn_cos, integral_sin_mul_cos₂, abs_cos_le_one, cos_sub_pi, cos_eq_zero_iff, rpow_eq_nhds_of_neg, mapsTo_cos, mapsTo_cos_Ioo, Complex.exp_re, one_add_mul_le_cos, cos_int_mul_two_pi, Complex.cos_ofReal_re, selfAdjoint.norm_sq_expUnitary_sub_one, tendsto_cos_pi_div_two, hasDerivAt_sin, Angle.cos_eq_real_cos_iff_eq_or_eq_neg, InnerProductGeometry.norm_div_cos_angle_sub_of_inner_eq_zero, Polynomial.Chebyshev.eval_T_real_eq_neg_one_iff, integral_sin_pow_three, cos_le_one_div_sqrt_sq_add_one, one_sub_sq_div_two_le_cos, analyticAt_cos, cos_add_int_mul_two_pi, cos_neg_of_pi_div_two_lt_of_lt, HasDerivWithinAt.sin, Polynomial.Chebyshev.isLocalMin_T_real, iteratedDerivWithin_cos_Icc, cos_arcsin, Polynomial.Chebyshev.integral_measureT_eq_integral_cos_of_continuous, Polynomial.isRoot_cos_pi_div_five, integral_cos_pow, cos_nat_mul_two_pi_sub_pi, sin_sub_pi_div_two, cos_add_two_pi, isIntegral_two_mul_cos_rat_mul_pi, EulerSine.integral_cos_mul_cos_pow_aux, antitoneOn_cos, cos_two_neg, cos_nat_mul_pi, fderivWithin_sin, continuous_tan, integral_sin_sq, ContDiff.cos, Polynomial.Chebyshev.T_real_cos, cos_pi_div_four, HasDerivWithinAt.cos, range_cos, cos_add_cos, sin_sub, cos_three_mul, cos_two_pi, integral_cos_pow_aux, hasSum_cos, cos_pi_div_sixteen, one_add_tan_sq_mul_cos_sq_eq_one, cos_two_pi_sub, sin_sq, inv_one_add_tan_sq, EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle, Complex.norm_mul_cos_arg, measurable_cos, HurwitzZeta.hasSum_nat_completedCosZeta, cos_le_one_sub_mul_cos_sq, cosPartialEquiv_apply, differentiable_cos, Complex.exp_ofReal_mul_I_re, InnerProductGeometry.cos_angle, cot_eq_cos_div_sin, cos_one_le, cos_nonpos_of_pi_div_two_le_of_le, Polynomial.Chebyshev.isLocalMax_T_real, tendsto_cos_neg_pi_div_two, cos_nonneg_of_mem_Icc, Polynomial.Chebyshev.S_two_mul_real_cos, InnerProductGeometry.cos_angle_mul_norm_mul_norm, HasStrictDerivAt.sin, Complex.cpow_ofReal_re, sq_cos_pi_div_six, abs_cos_int_mul_pi, abs_iteratedDeriv_cos_le_one, intervalIntegral.intervalIntegrable_cos, EulerSine.sin_pi_mul_eq, fderivWithin_cos, differentiableAt_cos, sin_pi_div_two_sub, integral_sin_pow_mul_cos_pow_odd, isAlgebraic_cos_rat_mul_pi, cos_pi_div_two, rpow_def_of_neg, hasDerivAt_tan, deriv_tan_sub_id, HasDerivAt.cos, EuclideanGeometry.cos_oangle_eq_cos_angle, iteratedDeriv_add_one_cos, cos_int_mul_pi_sub, sin_sq_eq_half_sub, sin_add, Measurable.cos, continuousOn_cos, cos_pi_div_eight, Quaternion.exp_of_re_eq_zero, HurwitzZeta.hasSum_nat_cosZeta, integral_sin_mul_cos₁, cos_eq_tsum, InnerProductGeometry.cos_eq_zero_iff_angle_eq_pi_div_two, Quaternion.re_exp, integral_sin_pow_aux, hasSum_one_div_nat_pow_mul_cos, cos_eq_cos_iff, derivWithin_cos, integral_sin_pow_even_mul_cos_pow_even, InnerProductGeometry.cos_eq_neg_one_iff_angle_eq_pi, sin_two_mul, cos_int_mul_two_pi_add_pi, hasDerivAt_cos, EulerSine.integral_sin_mul_sin_mul_cos_pow_eq, fderiv_cos, InnerProductGeometry.cos_angle_sub_of_inner_eq_zero, polarCoord_symm_apply, abs_sin_half, two_mul_cos_mul_cos, abs_sin_eq_sqrt_one_sub_cos_sq, Angle.cos_eq_iff_coe_eq_or_eq_neg, cos_add, cos_arcsin_nonneg, cos_one_pos, cos_pi_sub, cos_pi_div_six, sin_half_eq_neg_sqrt, differentiable_iteratedDeriv_cos, cos_eq_one_iff_of_lt_of_lt, Polynomial.Chebyshev.rootMultiplicity_T_real, DifferentiableOn.cos, Polynomial.Chebyshev.U_real_cos, sin_add_pi_div_two, contDiff_cos, cos_sub_nat_mul_two_pi, iteratedDeriv_even_cos, EuclideanGeometry.cos_angle_of_angle_eq_pi_div_two, EuclideanGeometry.cos_eq_neg_one_iff_angle_eq_pi, one_sub_mul_le_cos, Polynomial.Chebyshev.isMinOn_T_real, integral_cos_pow_three, abs_cos_sub_cos_le, Polynomial.Chebyshev.isLocalExtr_T_real_iff, analyticWithinAt_cos, bijOn_cos, cos_sq', cos_pos_of_mem_Ioo, Orientation.cos_oangle_eq_cos_angle, derivWithin_sin, cos_sub_int_mul_pi, InnerProductGeometry.cos_angle_add_mul_norm_of_inner_eq_zero, cos_pi_div_thirty_two, neg_one_le_cos, Polynomial.Chebyshev.isMaxOn_T_real, HasStrictFDerivAt.cos, ContDiffWithinAt.cos, deriv_cos, cos_nat_mul_pi_sub, Polynomial.Chebyshev.rootMultiplicity_U_real, continuous_cos, cos_eq_two_mul_tan_half_div_one_sub_tan_half_sq, EuclideanGeometry.cos_angle_mul_dist_of_angle_eq_pi_div_two, EulerSine.integral_cos_pow_eq, cos_arccos, HasFDerivAt.sin, integral_sin, sin_sq_add_cos_sq, Angle.cos_coe, Angle.cos_toReal, ContinuousLinearMap.rotation_apply, sin_sub_sin, EuclideanGeometry.cos_eq_zero_iff_angle_eq_pi_div_two, cos_sq_le_one, intervalIntegrable_log_cos, integral_sin_pow_odd_mul_cos_pow, EulerSine.tendsto_integral_cos_pow_mul_div, cos_lt_cos_of_nonneg_of_le_pi_div_two, cos_sq_add_sin_sq, cos_sub_cos, cos_nat_mul_two_pi_sub, cos_pi_over_two_pow, cos_eq_zero_iff_sin_eq, abs_cos_eq_sqrt_one_sub_sin_sq, hasStrictDerivAt_cos, cos_half, cos_neg, arccos_cos, integral_sin_mul_cos_sq, iteratedDeriv_add_one_sin, surjOn_cos, quadratic_root_cos_pi_div_five, cos_antiperiodic, cos_periodic, analyticOnNhd_cos, one_sub_sq_div_two_lt_cos, HasFDerivAt.cos, cos_sub_nat_mul_pi, EuclideanGeometry.dist_div_cos_angle_of_angle_eq_pi_div_two, Polynomial.Chebyshev.roots_T_real, deriv_cos, Complex.ofReal_cos, cos_lt_one_div_sqrt_sq_add_one, hasStrictDerivAt_sin, DifferentiableAt.cos, cos_add_pi_div_two, cos_sub_two_pi, cos_two_mul, tan_mul_cos, cos_int_mul_two_pi_sub_pi, deriv_cos', continuousOn_tan, hasDerivAt_tan_of_mem_Ioo, Polynomial.Chebyshev.eval_T_real_eq_one_iff, integral_sin_sq_mul_cos, lipschitzWith_cos, cos_eq_one_iff, EulerSine.integral_cos_pow_pos, cos_nonneg_of_neg_pi_div_two_le_of_le, cos_nat_mul_two_pi_add_pi, InnerProductGeometry.cos_eq_one_iff_angle_eq_zero, cos_sub_int_mul_two_pi, iteratedDeriv_odd_sin, EuclideanGeometry.law_cos, irrational_cos_rat_mul_pi, HasStrictFDerivAt.sin, strictAntiOn_cos, Complex.norm_exp_mul_exp_add_exp_neg_le_of_abs_im_le, cos_lt_cos_of_nonneg_of_le_pi, Complex.polarCoord_symm_apply, cos_sq, cos_int_mul_two_pi_sub, ContDiffAt.cos, hasStrictDerivAt_tan, rpow_def_of_nonpos, InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle, Polynomial.Chebyshev.isLocalExtr_T_real, deriv_sin, Polynomial.Chebyshev.isExtrOn_T_real, integral_sin_pow, HasStrictDerivAt.cos, InnerProductGeometry.cos_angle_sub_mul_norm_of_inner_eq_zero, cos_arctan_pos, cos_add_nat_mul_two_pi, integral_sin_sq_mul_cos_sq, InnerProductGeometry.inner_eq_cos_angle_of_norm_eq_one, isIntegral_two_mul_cos_rat_mul_pi, cos_eq_neg_one_iff, abs_cos_eq_one_iff, cos_sub, integral_cos_sq, cos_eq_sqrt_one_sub_sin_sq, cos_pi_div_three, cos_zero, EuclideanGeometry.cos_eq_one_iff_angle_eq_zero, AEMeasurable.cos, logDeriv_cos, cos_add_int_mul_pi, HasDerivAt.sin, cos_sub_pi_div_two, strictConcaveOn_cos_Icc, HasFDerivWithinAt.cos, integral_cos_sq_sub_sin_sq, deriv_sin, injOn_cos, HurwitzZeta.hasSum_nat_cosKernel₀, cos_nat_mul_two_pi, cos_le_cos_of_nonneg_of_le_pi, cos_sq_arctan, Polynomial.Chebyshev.roots_U_real_nodup, cos_pi, cos_pos_of_le_one, deriv_tan, cos_int_mul_pi, Polynomial.Chebyshev.roots_T_real_nodup, cos_pi_div_two_sub, Differentiable.cos, cos_mem_Icc, sin_half_eq_sqrt, sin_eq_sqrt_one_sub_cos_sq, two_mul_sin_mul_sin, range_cos_infinite, cos_two_mul', Polynomial.Chebyshev.C_two_mul_real_cos, unitary.two_mul_one_sub_cos_norm_argSelfAdjoint, Polynomial.Chebyshev.roots_U_real, HasFDerivWithinAt.sin, cos_le_one, fderiv_sin, Complex.cos_arg, EulerSine.integral_cos_mul_cos_pow_even, Quaternion.exp_eq, cos_bound, cos_abs, Polynomial.Chebyshev.abs_eval_T_real_eq_one_iff, tan_eq_sin_div_cos, two_mul_sin_mul_cos, Complex.cpow_ofReal, Polynomial.Chebyshev.eval_T_real_cos_int_mul_pi_div, DifferentiableWithinAt.cos, cos_arctan, exists_cos_eq_zero, InnerProductGeometry.norm_div_cos_angle_add_of_inner_eq_zero, Unitary.two_mul_one_sub_cos_norm_argSelfAdjoint
cosh 📖	CompOp	108 math math: one_le_cosh, exp_sub_sinh, sinh_add, HasDerivWithinAt.cosh, Differentiable.cosh, analyticOn_cosh, ContDiffOn.cosh, cosh_abs, iteratedDeriv_even_cosh, ContDiffWithinAt.cosh, derivWithin_cosh, fderivWithin_sinh, hasStrictDerivAt_sinh, cosh_surjOn, hasSum_cosh, tanh_eq_sinh_div_cosh, deriv_sinh, cosh_arcosh, UpperHalfPlane.center_im, analyticOnNhd_cosh, continuous_cosh, UpperHalfPlane.cosh_dist, UpperHalfPlane.dist_coe_center, iteratedDeriv_add_one_cosh, iteratedDeriv_add_one_sinh, HasDerivAt.cosh, hasStrictDerivAt_cosh, HasStrictDerivAt.cosh, ContDiffAt.cosh, cosh_sq, UpperHalfPlane.dist_self_center, Polynomial.Chebyshev.S_two_mul_real_cosh, exp_mul_le_cosh_add_mul_sinh, HasDerivAt.sinh, sinh_sq, sinh_sub, exp_sub_cosh, iteratedDeriv_odd_sinh, measurable_cosh, cosh_zero, differentiableAt_cosh, Measurable.cosh, deriv_sinh, DifferentiableAt.cosh, HasFDerivWithinAt.sinh, cosh_pos, sinh_two_mul, cosh_le_exp_half_sq, cosh_add_sinh, DifferentiableWithinAt.cosh, cosh_bijOn, HasFDerivAt.sinh, differentiable_cosh, HasDerivWithinAt.sinh, one_lt_cosh, cosh_lt_cosh, cosh_sub, sinh_sub_cosh, iteratedDeriv_odd_cosh, hasDerivAt_cosh, cosh_le_cosh, fderiv_sinh, UpperHalfPlane.cosh_half_dist, Polynomial.Chebyshev.T_real_cosh, arcosh_cosh, cosh_strictMonoOn, cosh_arsinh, cosh_three_mul, DifferentiableOn.cosh, contDiff_cosh, differentiable_iteratedDeriv_cosh, analyticAt_cosh, sinh_lt_cosh, cosh_sq', cosh_log, Polynomial.Chebyshev.U_real_cosh, iteratedDerivWithin_cosh_Icc, HasStrictDerivAt.sinh, cosh_sub_sinh, sinh_add_cosh, fderivWithin_cosh, cosh_injOn, UpperHalfPlane.dist_coe_center_sq, iteratedDerivWithin_cosh_Ioo, Complex.ofReal_cosh, cosh_eq, UpperHalfPlane.cosh_dist', HasStrictFDerivAt.cosh, cosh_sq_sub_sinh_sq, analyticWithinAt_cosh, fderiv_cosh, HasStrictFDerivAt.sinh, cosh_eq_tsum, HasFDerivAt.cosh, derivWithin_sinh, Complex.cosh_ofReal_re, cosh_add, logDeriv_cosh, hasDerivAt_sinh, cosh_neg, deriv_cosh, cosh_two_mul, cosh_artanh, AEMeasurable.cosh, deriv_cosh, ContDiff.cosh, HasFDerivWithinAt.cosh, Polynomial.Chebyshev.C_two_mul_real_cosh
cot 📖	CompOp	5 math math: tan_inv_eq_cot, Complex.ofReal_cot, cot_eq_cos_div_sin, logDeriv_sin, cot_inv_eq_tan
sin 📖	CompOp	310 math math: range_sin, sin_add_sin, sin_le_sin_of_le_of_le_pi_div_two, sin_arctan, sin_eq_zero_iff_cos_eq, integral_cos, iteratedDeriv_odd_cos, sin_pi_div_two, sin_add_two_pi, integral_sin_mul_cos₂, analyticOnNhd_sin, sin_periodic, lt_sin, EuclideanGeometry.law_sin, InnerProductGeometry.sin_angle, range_sin_infinite, sin_arctan_nonneg, isIntegral_two_mul_sin_rat_mul_pi, hasDerivAt_sin, integral_log_sin_zero_pi_div_two, sin_two_pi, integral_sin_pow_three, sin_lt, sin_le_one, abs_sin_eq_sin_abs_of_abs_le_pi, sin_pi_sub, sin_pi, sinc_eq_dslope, integral_sin_pow_pos, sin_arcsin, sin_pi_div_three, HasDerivWithinAt.sin, InnerProductGeometry.sin_angle_div_norm_eq_sin_angle_div_norm, sin_add_int_mul_pi, integral_cos_pow, sin_antiperiodic, sin_sub_pi_div_two, HurwitzZeta.hasSum_nat_sinZeta, sin_gt_sub_cube, EulerSine.integral_cos_mul_cos_pow_aux, sin_add_nat_mul_pi, sin_lt_sin_of_lt_of_le_pi_div_two, fderivWithin_sin, Affine.Triangle.dist_div_sin_angle_eq_two_mul_circumradius, integral_sin_sq, HasDerivWithinAt.cos, InnerProductGeometry.sin_angle_mul_norm_eq_sin_angle_mul_norm, sin_sq_arctan, sin_pos_of_pos_of_le_two, Gamma_mul_Gamma_one_sub, sin_sub, mul_le_sin, integral_cos_pow_aux, intervalIntegral.intervalIntegrable_sin, InnerProductGeometry.sin_angle_nonneg, Complex.norm_exp_I_mul_ofReal_sub_one, InnerProductGeometry.sin_eq_one_iff_angle_eq_pi_div_two, sin_sq, InnerProductGeometry.norm_toLp_symm_crossProduct, sin_arcsin', tan_div_sqrt_one_add_tan_sq, cot_eq_cos_div_sin, analyticAt_sin, Differentiable.sin, Polynomial.Chebyshev.S_two_mul_real_cos, HasStrictDerivAt.sin, sin_nonneg_of_nonneg_of_le_pi, InnerProductGeometry.sin_angle_sub_of_inner_eq_zero, tendsto_sin_neg_pi_div_two, le_arcsin_iff_sin_le', ContDiff.sin, sin_zero, HurwitzZeta.hasSum_nat_sinKernel, isEquivalent_sin, sin_nat_mul_two_pi_sub, fderivWithin_cos, sin_pi_div_two_sub, InnerProductGeometry.sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi, integral_sin_pow_mul_cos_pow_odd, EuclideanGeometry.sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi, Angle.sin_eq_iff_coe_eq_or_add_eq_pi, HasDerivAt.cos, iteratedDeriv_add_one_cos, sin_eq_tsum, sin_arctan_pos, sin_sq_eq_half_sub, sin_add, sin_neg, integral_exp_mul_I_eq_sin, tan_sq_div_one_add_tan_sq, Quaternion.exp_of_re_eq_zero, arcsin_lt_iff_lt_sin, lipschitzWith_sin, integral_sin_mul_cos₁, continuous_sin, arcsin_le_iff_le_sin', integral_sin_pow_aux, Wallis.W_eq_integral_sin_pow_div_integral_sin_pow, DifferentiableWithinAt.sin, sin_nat_mul_pi, abs_sin_sub_sin_le, hasStrictDerivAt_const_rpow_of_neg, derivWithin_cos, EuclideanGeometry.sin_eq_one_iff_angle_eq_pi_div_two, integral_sin_pow_even_mul_cos_pow_even, sin_two_pi_sub, EuclideanGeometry.sin_angle_div_dist_eq_sin_angle_div_dist, sinOrderIso_apply, AEMeasurable.sin, sin_two_mul, InnerProductGeometry.norm_ofLp_crossProduct, iteratedDerivWithin_sin_Icc, sin_pos_of_pos_of_lt_pi, Complex.exp_ofReal_mul_I_im, hasDerivAt_cos, sin_eq_sin_iff, EulerSine.integral_sin_mul_sin_mul_cos_pow_eq, fderiv_cos, InnerProductGeometry.norm_div_sin_angle_add_of_inner_eq_zero, polarCoord_symm_apply, sin_nonneg_of_mem_Icc, EuclideanGeometry.dist_div_sin_angle_of_angle_eq_pi_div_two, abs_sin_half, abs_sin_eq_sqrt_one_sub_cos_sq, cos_add, ContDiffOn.sin, sin_nonpos_of_nonpos_of_neg_pi_le, contDiff_sin, sin_int_mul_two_pi_sub, sin_half_eq_neg_sqrt, InnerProductGeometry.sin_angle_sub_mul_norm_of_inner_eq_zero, sin_int_mul_pi_sub, Polynomial.Chebyshev.U_real_cos, sin_add_pi_div_two, EuclideanGeometry.sin_angle_of_angle_eq_pi_div_two, Complex.sin_ofReal_re, continuousOn_sin, EuclideanGeometry.collinear_iff_eq_or_eq_or_sin_eq_zero, lt_arcsin_iff_sin_lt, HurwitzZeta.hasSum_nat_completedSinZeta, integral_cos_pow_three, lt_arcsin_iff_sin_lt', Quaternion.im_exp, sin_pi_over_two_pow_succ, bijOn_sin, EuclideanGeometry.sin_angle_mul_dist_eq_sin_angle_mul_dist, cos_sq', differentiable_sin, mul_abs_le_abs_sin, InnerProductGeometry.norm_div_sin_angle_sub_of_inner_eq_zero, derivWithin_sin, integral_log_sin_zero_pi, sin_div_le_inv_abs, sin_sub_int_mul_pi, EuclideanGeometry.dist_eq_dist_mul_sin_angle_div_sin_angle, abs_sin_lt_abs, DifferentiableAt.sin, sin_sq_le_sq, sin_sq_le_one, HasStrictFDerivAt.cos, Angle.sin_coe, deriv_cos, le_sin, sin_bound, surjOn_sin, sin_pi_div_thirty_two, sin_pi_div_six, EulerSine.integral_cos_pow_eq, analyticOn_sin, sin_sub_pi, HasFDerivAt.sin, integral_sin, sin_sq_add_cos_sq, EuclideanGeometry.sin_angle_mul_dist_of_angle_eq_pi_div_two, sin_arctan_eq_zero, injOn_sin, ContinuousLinearMap.rotation_apply, sin_sub_sin, lt_sin_mul, integral_sin_pow_odd_mul_cos_pow, cos_sq_add_sin_sq, cos_sub_cos, arcsin_sin, sin_arccos, cos_eq_zero_iff_sin_eq, abs_cos_eq_sqrt_one_sub_sin_sq, hasStrictDerivAt_cos, mapsTo_sin, isAlgebraic_sin_rat_mul_pi, integral_sin_mul_cos_sq, iteratedDeriv_add_one_sin, differentiable_iteratedDeriv_sin, iteratedDeriv_even_sin, HasFDerivAt.cos, arcsin_lt_iff_lt_sin', sin_three_mul, le_arcsin_iff_sin_le, sin_add_nat_mul_two_pi, hasSum_one_div_nat_pow_mul_sin, mul_lt_sin, neg_one_le_sin, deriv_cos, abs_sin_eq_one_iff, mapsTo_sin_Ioo, sin_pos_of_mem_Ioo, abs_iteratedDeriv_sin_le_one, sin_arctan_strictMono, Complex.cpow_ofReal_im, sin_eq_neg_one_iff, sin_pi_div_sixteen, hasStrictDerivAt_sin, cos_add_pi_div_two, integral_sin_pow_succ_le, tan_mul_cos, logDeriv_sin, DifferentiableOn.sin, deriv_cos', sin_sub_nat_mul_pi, strictConcaveOn_sin_Icc, InnerProductGeometry.sin_angle_add_of_inner_eq_zero, sin_sq_lt_sq, integral_sin_sq_mul_cos, hasSum_sin, measurable_sin, sin_sq_pi_over_two_pow, sq_sin_pi_div_three, abs_sin_le_abs, Complex.ofReal_sin, arcsin_sin', monotoneOn_sin, abs_sin_le_one, analyticWithinAt_sin, sin_nat_mul_pi_sub, Affine.Triangle.dist_div_sin_angle_div_two_eq_circumradius, sin_eq_zero_iff, sinc_of_ne_zero, sin_arctan_le_zero, ContDiffAt.sin, iteratedDeriv_odd_sin, sinc_apply, integral_sin_pow_odd, HasStrictFDerivAt.sin, Complex.polarCoord_symm_apply, Measurable.sin, arcsin_eq_iff_eq_sin, sin_neg_of_neg_of_neg_pi_lt, tendsto_euler_sin_prod, sin_pi_div_eight, deriv_sin, tendsto_sin_pi_div_two, integral_sin_pow, strictMonoOn_sin, HasStrictDerivAt.cos, integral_sin_sq_mul_cos_sq, sin_sub_two_pi, cos_sub, integral_cos_sq, HurwitzZeta.LSeriesHasSum_sin, cos_eq_sqrt_one_sub_sin_sq, hasStrictFDerivAt_rpow_of_neg, arcsin_le_iff_le_sin, le_sin_mul, ContDiffWithinAt.sin, EuclideanGeometry.sin_pos_of_not_collinear, sin_add_pi, sin_le, HasDerivAt.sin, Angle.sin_eq_real_sin_iff_eq_or_add_eq_pi, sin_sub_int_mul_two_pi, differentiableAt_sin, InnerProductGeometry.sin_angle_add, cos_sub_pi_div_two, HasFDerivWithinAt.cos, integral_cos_sq_sub_sin_sq, InnerProductGeometry.sin_angle_add_mul_norm_of_inner_eq_zero, deriv_sin, sin_eq_one_iff, sin_mem_Icc, sin_add_int_mul_two_pi, Angle.sin_toReal, sin_pos_of_pos_of_le_one, cos_pi_div_two_sub, InnerProductGeometry.sin_angle_mul_norm_mul_norm, integral_sin_pow_antitone, intervalIntegrable_log_sin, sin_half_eq_sqrt, sin_eq_sqrt_one_sub_cos_sq, two_mul_sin_mul_sin, sin_le_mul, cos_two_mul', sin_eq_two_mul_tan_half_div_one_add_tan_half_sq, Complex.sin_arg, Complex.exp_im, HasFDerivWithinAt.sin, fderiv_sin, integral_sin_pow_even, Quaternion.exp_eq, hasSum_L_function_mod_four_eval_three, sin_int_mul_pi, tan_eq_sin_div_cos, iteratedDerivWithin_sin_Ioo, two_mul_sin_mul_cos, Complex.cpow_ofReal, coe_sinOrderIso_apply, sin_eq_zero_iff_of_lt_of_lt, sin_pi_div_four, sin_arctan_lt_zero, Complex.norm_mul_sin_arg, sin_sq_pi_over_two_pow_succ, sin_sub_nat_mul_two_pi
sinh 📖	CompOp	128 math math: sinh_eq, sinh_log, exp_sub_sinh, sinh_add, measurable_sinh, HasDerivWithinAt.cosh, UpperHalfPlane.image_coe_sphere, sinh_nonneg_iff, sinh_surjective, differentiable_sinh, UpperHalfPlane.dist_le_iff_dist_coe_center_le, derivWithin_cosh, fderivWithin_sinh, hasStrictDerivAt_sinh, analyticWithinAt_sinh, abs_sinh, sinh_zero, hasSum_sinh, sinh_arcosh, analyticAt_sinh, tanh_eq_sinh_div_cosh, UpperHalfPlane.dist_eq_iff_eq_sinh, Differentiable.sinh, sinh_inj, ContDiffAt.sinh, deriv_sinh, UpperHalfPlane.dist_eq_iff_eq_sq_sinh, UpperHalfPlane.image_coe_ball, sinh_sub_id_strictMono, UpperHalfPlane.image_coe_closedBall, self_lt_sinh_iff, UpperHalfPlane.dist_coe_center, iteratedDeriv_add_one_cosh, sinh_lt_self_iff, iteratedDeriv_add_one_sinh, HasDerivAt.cosh, UpperHalfPlane.lt_dist_iff_lt_dist_coe_center, sinh_arsinh, Measurable.sinh, hasStrictDerivAt_cosh, HasStrictDerivAt.cosh, sinhEquiv_apply, UpperHalfPlane.dist_lt_iff_dist_coe_center_lt, cosh_sq, sinh_eq_tsum, sinh_neg, iteratedDerivWithin_sinh_Icc, sinh_eq_zero, Polynomial.Chebyshev.S_two_mul_real_cosh, exp_mul_le_cosh_add_mul_sinh, HasDerivAt.sinh, sinh_sq, sinh_sub, exp_sub_cosh, ContDiffWithinAt.sinh, iteratedDeriv_odd_sinh, DifferentiableOn.sinh, deriv_sinh, HasFDerivWithinAt.sinh, continuous_sinh, UpperHalfPlane.dist_eq_iff_dist_coe_center_eq, UpperHalfPlane.cmp_dist_eq_cmp_dist_coe_center, Complex.sinh_ofReal_re, sinh_two_mul, sinhOrderIso_apply, cosh_add_sinh, self_le_sinh_iff, HasFDerivAt.sinh, UpperHalfPlane.le_dist_iff_le_dist_coe_center, sinh_lt_sinh, HasDerivWithinAt.sinh, UpperHalfPlane.dist_center_dist, cosh_sub, sinh_sub_cosh, iteratedDeriv_odd_cosh, hasDerivAt_cosh, iteratedDerivWithin_sinh_Ioo, iteratedDeriv_even_sinh, contDiff_sinh, fderiv_sinh, Complex.ofReal_sinh, AEMeasurable.sinh, UpperHalfPlane.sinh_half_dist_add_dist, sinh_neg_iff, sinh_lt_cosh, cosh_sq', Polynomial.Chebyshev.U_real_cosh, sinh_strictMono, HasStrictDerivAt.sinh, cosh_sub_sinh, DifferentiableAt.sinh, sinh_add_cosh, sinh_injective, analyticOn_sinh, differentiableAt_sinh, differentiable_iteratedDeriv_sinh, fderivWithin_cosh, ContDiff.sinh, UpperHalfPlane.sinh_half_dist, UpperHalfPlane.dist_le_iff_le_sinh, sinh_pos_iff, arsinh_sinh, UpperHalfPlane.dist_coe_center_sq, sinh_le_sinh, HasStrictFDerivAt.cosh, analyticOnNhd_sinh, cosh_sq_sub_sinh_sq, fderiv_cosh, HasStrictFDerivAt.sinh, sinh_three_mul, HasFDerivAt.cosh, derivWithin_sinh, cosh_add, hasDerivAt_sinh, deriv_cosh, DifferentiableWithinAt.sinh, sinh_nonpos_iff, cosh_two_mul, sinh_artanh, Mathlib.Meta.Positivity.sinh_pos_of_pos, deriv_cosh, sinh_bijective, sinhHomeomorph_apply, Mathlib.Meta.Positivity.sinh_nonneg_of_nonneg, ContDiffOn.sinh, HasFDerivWithinAt.cosh, isEquivalent_sinh, sinh_le_self_iff
tan 📖	CompOp	91 math math: tan_pi_div_four, tan_pi_sub, tan_nonpos_of_nonpos_of_neg_pi_div_two_le, tan_inv_eq_cot, tan_int_mul_pi, le_tan, continuousAt_tan, tan_sub', contDiffAt_tan, InnerProductGeometry.tan_angle_sub_mul_norm_of_inner_eq_zero, tan_arccos, tan_int_mul_pi_div_two, Complex.tan_arg, InnerProductGeometry.tan_angle_add_mul_norm_of_inner_eq_zero, tan_neg, continuous_tan, tan_neg_of_neg_of_pi_div_two_lt, tan_nat_mul_pi_sub, Complex.tan_ofReal_re, tan_two_mul, one_add_tan_sq_mul_cos_sq_eq_one, inv_one_add_tan_sq, tan_div_sqrt_one_add_tan_sq, EuclideanGeometry.dist_div_tan_angle_of_angle_eq_pi_div_two, tan_pi_div_two, coe_tanPartialHomeomorph, isAlgebraic_tan_rat_mul_pi, hasDerivAt_tan, tan_add, deriv_tan_sub_id, tan_sub_pi, InnerProductGeometry.norm_div_tan_angle_sub_of_inner_eq_zero, tan_sq_div_one_add_tan_sq, injOn_tan, tan_lt_tan_of_nonneg_of_lt_pi_div_two, tan_lt_tan_of_lt_of_lt_pi_div_two, InnerProductGeometry.norm_div_tan_angle_add_of_inner_eq_zero, InnerProductGeometry.tan_angle_sub_of_inner_eq_zero, tan_pi_div_two_sub, tan_eq_one_sub_tan_half_sq_div_one_add_tan_half_sq, InnerProductGeometry.tan_angle_add_of_inner_eq_zero, tan_periodic, lt_tan, tan_nat_mul_pi, tan_add_int_mul_pi, tan_pi_div_six, EuclideanGeometry.tan_angle_of_angle_eq_pi_div_two, tendsto_abs_tan_of_cos_eq_zero, differentiableAt_tan, tan_nonneg_of_nonneg_of_le_pi_div_two, tendsto_tan_pi_div_two, inv_sqrt_one_add_tan_sq, cos_eq_two_mul_tan_half_div_one_sub_tan_half_sq, image_tan_Ioo, EuclideanGeometry.tan_angle_mul_dist_of_angle_eq_pi_div_two, tan_add', tendsto_tan_neg_pi_div_two, tan_int_mul_pi_sub, differentiableAt_tan_of_mem_Ioo, tan_pi_div_three, tan_eq_zero_iff, tan_mul_cos, continuousOn_tan, hasDerivAt_tan_of_mem_Ioo, tan_surjective, tan_sub_nat_mul_pi, tendsto_abs_tan_atTop, tan_arctan, tan_eq_zero_of_cos_eq_zero, hasStrictDerivAt_tan, tan_add_nat_mul_pi, strictMonoOn_tan, tan_sub, logDeriv_cos, tan_arcsin, surjOn_tan, tan_pi, Angle.tan_toReal, cot_inv_eq_tan, tan_sub_int_mul_pi, deriv_tan, tan_zero, arctan_tan, sin_eq_two_mul_tan_half_div_one_add_tan_half_sq, tan_pos_of_pos_of_lt_pi_div_two, tan_eq_zero_iff', tan_eq_sin_div_cos, tan_add_pi, Complex.ofReal_tan, continuousOn_tan_Ioo, Angle.tan_coe
tanh 📖	CompOp	19 math math: abs_tanh_lt_one, Complex.ofReal_tanh, tanh_eq_sinh_div_cosh, tanh_arcosh, neg_one_lt_tanh, Complex.tanh_ofReal_re, tanh_artanh, tanh_lt_one, tanh_eq, tanh_sq_lt_one, UpperHalfPlane.tanh_half_dist, tanh_arsinh, tanh_zero, tanh_injective, logDeriv_cosh, tanh_surjOn, tanh_neg, tanh_bijOn, artanh_tanh

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_cos_eq_sqrt_one_sub_sin_sq 📖	mathematical	—	abs Real lattice instAddGroup cos sqrt instSub instOne Monoid.toNatPow instMonoid sin	—	cos_sq' sqrt_sq_eq_abs
abs_cos_le_one 📖	mathematical	—	Real instLE abs lattice instAddGroup cos instOne	—	abs_le_one_iff_mul_self_le_one instIsStrictOrderedRing
abs_sin_eq_sqrt_one_sub_cos_sq 📖	mathematical	—	abs Real lattice instAddGroup sin sqrt instSub instOne Monoid.toNatPow instMonoid cos	—	sin_sq sqrt_sq_eq_abs
abs_sin_le_one 📖	mathematical	—	Real instLE abs lattice instAddGroup sin instOne	—	abs_le_one_iff_mul_self_le_one instIsStrictOrderedRing
abs_tanh_lt_one 📖	mathematical	—	Real instLT abs lattice instAddGroup tanh instOne	—	abs_lt IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add neg_one_lt_tanh tanh_lt_one
cos_abs 📖	mathematical	—	cos abs Real lattice instAddGroup	—	le_total abs_of_nonpos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid cos_neg abs_of_nonneg
cos_add 📖	mathematical	—	cos Real instAdd instSub instMul sin	—	Complex.ofReal_injective Complex.ofReal_cos Complex.ofReal_add Complex.cos_add Complex.ofReal_sub Complex.ofReal_mul Complex.ofReal_sin
cos_add_cos 📖	mathematical	—	Real instAdd cos instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv instDivInvMonoid instSub	—	Complex.ofReal_injective Nat.instAtLeastTwoHAddOfNat Complex.ofReal_add Complex.ofReal_cos Complex.cos_add_cos Complex.ofReal_mul Complex.ofReal_div Complex.ofReal_sub
cos_bound 📖	mathematical	Real instLE abs lattice instAddGroup instOne	instSub cos DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instMul	—	Nat.instAtLeastTwoHAddOfNat Complex.ofReal_sub Complex.ofReal_div Complex.ofReal_pow Complex.cos_bound Complex.norm_real
cos_le_one 📖	mathematical	—	Real instLE cos instOne	—	abs_le instIsOrderedAddMonoid abs_cos_le_one
cos_neg 📖	mathematical	—	cos Real instNeg	—	Complex.ofReal_neg Complex.cos_neg
cos_one_le 📖	mathematical	—	Real instLE cos instOne DivInvMonoid.toDiv instDivInvMonoid instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat sub_le_iff_le_add covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid abs_sub_le_iff cos_bound abs_one instIsOrderedRing Mathlib.Meta.NormNum.isRat_le_true instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.isNat_abs_nonneg Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.one_natPow Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub
cos_one_pos 📖	mathematical	—	Real instLT instZero cos instOne	—	cos_pos_of_le_one le_of_eq abs_one instIsOrderedRing
cos_pos_of_le_one 📖	mathematical	Real instLE abs lattice instAddGroup instOne	instLT instZero cos	—	Nat.instAtLeastTwoHAddOfNat sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid lt_sub_iff_add_lt add_le_add mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono instIsOrderedRing pow_le_one₀ IsOrderedRing.toPosMulMono abs_nonneg le_of_lt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono sq abs_mul_self abs_mul mul_le_one₀ Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_inv_pos sub_le_comm abs_sub_le_iff cos_bound
cos_sq 📖	mathematical	—	Real Monoid.toNatPow instMonoid cos instAdd DivInvMonoid.toDiv instDivInvMonoid instOne instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instMul	—	Complex.ofReal_injective Nat.instAtLeastTwoHAddOfNat Complex.ofReal_pow Complex.ofReal_cos Complex.cos_sq one_div Complex.ofReal_add Complex.ofReal_inv Complex.ofReal_div Complex.ofReal_mul
cos_sq' 📖	mathematical	—	Real Monoid.toNatPow instMonoid cos instSub instOne sin	—	sin_sq_add_cos_sq add_sub_cancel_left
cos_sq_add_sin_sq 📖	mathematical	—	Real instAdd Monoid.toNatPow instMonoid cos sin instOne	—	add_comm sin_sq_add_cos_sq
cos_sq_le_one 📖	mathematical	—	Real instLE Monoid.toNatPow instMonoid cos instOne	—	sin_sq_add_cos_sq le_add_of_nonneg_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono instIsOrderedRing
cos_sub 📖	mathematical	—	cos Real instSub instAdd instMul sin	—	sub_eq_add_neg cos_add cos_neg sin_neg mul_neg neg_neg
cos_sub_cos 📖	mathematical	—	Real instSub cos instMul instNeg instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat sin DivInvMonoid.toDiv instDivInvMonoid instAdd	—	Complex.ofReal_injective Nat.instAtLeastTwoHAddOfNat Complex.ofReal_sub Complex.ofReal_cos Complex.cos_sub_cos neg_mul Complex.ofReal_neg Complex.ofReal_mul Complex.ofReal_sin Complex.ofReal_div Complex.ofReal_add
cos_three_mul 📖	mathematical	—	cos Real instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instSub Monoid.toNatPow instMonoid	—	Nat.instAtLeastTwoHAddOfNat Complex.ofReal_cos Complex.ofReal_mul Complex.cos_three_mul Complex.ofReal_sub Complex.ofReal_pow
cos_two_mul 📖	mathematical	—	cos Real instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instSub Monoid.toNatPow instMonoid instOne	—	Complex.ofReal_injective Nat.instAtLeastTwoHAddOfNat Complex.ofReal_cos Complex.ofReal_mul Complex.cos_two_mul Complex.ofReal_sub Complex.ofReal_pow
cos_two_mul' 📖	mathematical	—	cos Real instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instSub Monoid.toNatPow instMonoid sin	—	Complex.ofReal_injective Nat.instAtLeastTwoHAddOfNat Complex.ofReal_cos Complex.ofReal_mul Complex.cos_two_mul' Complex.ofReal_sub Complex.ofReal_pow Complex.ofReal_sin
cos_two_neg 📖	mathematical	—	Real instLT cos instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instZero	—	Nat.instAtLeastTwoHAddOfNat mul_one cos_two_mul sub_le_sub_right covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono instIsOrderedRing pow_le_pow_left₀ IsOrderedRing.toMulPosMono LT.lt.le cos_one_pos cos_one_le le_of_lt Mathlib.Meta.Positivity.pos_of_isNat instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isRat_lt_true instIsStrictOrderedRing DivisionRing.toNontrivial Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_pow Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Nat.cast_one Nat.cast_zero
cos_zero 📖	mathematical	—	cos Real instZero instOne	—	Complex.cos_zero
cosh_abs 📖	mathematical	—	cosh abs Real lattice instAddGroup	—	le_total abs_of_nonpos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid cosh_neg abs_of_nonneg
cosh_add 📖	mathematical	—	cosh Real instAdd instMul sinh	—	Complex.ofReal_cosh Complex.ofReal_add Complex.cosh_add Complex.ofReal_mul Complex.ofReal_sinh
cosh_add_sinh 📖	mathematical	—	Real instAdd cosh sinh exp	—	Complex.ofReal_add Complex.ofReal_cosh Complex.ofReal_sinh Complex.cosh_add_sinh Complex.ofReal_exp
cosh_eq 📖	mathematical	—	cosh Real DivInvMonoid.toDiv instDivInvMonoid instAdd exp instNeg instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	eq_div_of_mul_eq Nat.instAtLeastTwoHAddOfNat two_ne_zero CharZero.NeZero.two IsStrictOrderedRing.toCharZero instIsStrictOrderedRing cosh.eq_1 exp.eq_1 Complex.ofReal_neg Complex.cosh.eq_1 mul_two Complex.add_re div_mul_cancel₀ two_ne_zero' Complex.instCharZero
cosh_neg 📖	mathematical	—	cosh Real instNeg	—	Complex.ofReal_cosh Complex.ofReal_neg Complex.cosh_neg
cosh_pos 📖	mathematical	—	Real instLT instZero cosh	—	Nat.instAtLeastTwoHAddOfNat half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing add_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid exp_pos cosh_eq
cosh_sq 📖	mathematical	—	Real Monoid.toNatPow instMonoid cosh instAdd sinh instOne	—	Complex.ofReal_pow Complex.ofReal_cosh Complex.cosh_sq Complex.ofReal_add Complex.ofReal_sinh
cosh_sq' 📖	mathematical	—	Real Monoid.toNatPow instMonoid cosh instAdd instOne sinh	—	cosh_sq add_comm
cosh_sq_sub_sinh_sq 📖	mathematical	—	Real instSub Monoid.toNatPow instMonoid cosh sinh instOne	—	Complex.ofReal_sub Complex.ofReal_pow Complex.ofReal_cosh Complex.ofReal_sinh Complex.cosh_sq_sub_sinh_sq
cosh_sub 📖	mathematical	—	cosh Real instSub instMul sinh	—	sub_eq_add_neg cosh_add cosh_neg sinh_neg mul_neg
cosh_sub_sinh 📖	mathematical	—	Real instSub cosh sinh exp instNeg	—	Complex.ofReal_sub Complex.ofReal_cosh Complex.ofReal_sinh Complex.cosh_sub_sinh Complex.ofReal_exp Complex.ofReal_neg
cosh_three_mul 📖	mathematical	—	cosh Real instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instSub Monoid.toNatPow instMonoid	—	Nat.instAtLeastTwoHAddOfNat Complex.ofReal_cosh Complex.ofReal_mul Complex.cosh_three_mul Complex.ofReal_sub Complex.ofReal_pow
cosh_two_mul 📖	mathematical	—	cosh Real instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instAdd Monoid.toNatPow instMonoid sinh	—	Nat.instAtLeastTwoHAddOfNat Complex.ofReal_cosh Complex.ofReal_mul Complex.cosh_two_mul Complex.ofReal_add Complex.ofReal_pow Complex.ofReal_sinh
cosh_zero 📖	mathematical	—	cosh Real instZero instOne	—	Complex.cosh_zero
cot_eq_cos_div_sin 📖	mathematical	—	cot Real DivInvMonoid.toDiv instDivInvMonoid cos sin	—	Complex.ofReal_injective Complex.ofReal_cot Complex.ofReal_div Complex.ofReal_cos Complex.ofReal_sin
cot_inv_eq_tan 📖	mathematical	—	Real instInv cot tan	—	Complex.ofReal_injective Complex.ofReal_inv Complex.ofReal_cot Complex.cot_inv_eq_tan Complex.ofReal_tan
exp_sub_cosh 📖	mathematical	—	Real instSub exp cosh sinh	—	sub_eq_iff_eq_add sinh_add_cosh
exp_sub_sinh 📖	mathematical	—	Real instSub exp sinh cosh	—	sub_eq_iff_eq_add cosh_add_sinh
inv_one_add_tan_sq 📖	mathematical	—	Real instInv instAdd instOne Monoid.toNatPow instMonoid tan cos	—	Complex.ofReal_inv Complex.ofReal_add Complex.ofReal_pow Complex.ofReal_tan Complex.ofReal_cos Complex.inv_one_add_tan_sq
inv_sqrt_one_add_tan_sq 📖	mathematical	Real instLT instZero cos	instInv sqrt instAdd instOne Monoid.toNatPow instMonoid tan	—	sqrt_sq LT.lt.le sqrt_inv inv_one_add_tan_sq LT.lt.ne'
neg_one_le_cos 📖	mathematical	—	Real instLE instNeg instOne cos	—	abs_le instIsOrderedAddMonoid abs_cos_le_one
neg_one_le_sin 📖	mathematical	—	Real instLE instNeg instOne sin	—	abs_le instIsOrderedAddMonoid abs_sin_le_one
neg_one_lt_tanh 📖	mathematical	—	Real instLT instNeg instOne tanh	—	tanh_eq Mathlib.Tactic.FieldSimp.lt_eq_cancel_lt IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg LT.lt.ne' add_pos' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid exp_pos one_mul mul_neg Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.cons_pos instZeroLEOneClass zero_lt_one NeZero.one GroupWithZero.toNontrivial
one_add_tan_sq_mul_cos_sq_eq_one 📖	mathematical	—	Real instMul instAdd instOne Monoid.toNatPow instMonoid tan cos	—	Nat.cast_one Complex.one_add_tan_sq_mul_cos_sq_eq_one Nat.cast_zero
sin_add 📖	mathematical	—	sin Real instAdd instMul cos	—	Complex.ofReal_injective Complex.ofReal_sin Complex.ofReal_add Complex.sin_add Complex.ofReal_mul Complex.ofReal_cos
sin_add_sin 📖	mathematical	—	Real instAdd sin instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv instDivInvMonoid cos instSub	—	Complex.ofReal_injective Nat.instAtLeastTwoHAddOfNat Complex.ofReal_add Complex.ofReal_sin Complex.sin_add_sin Complex.ofReal_mul Complex.ofReal_div Complex.ofReal_cos Complex.ofReal_sub
sin_bound 📖	mathematical	Real instLE abs lattice instAddGroup instOne	instSub sin DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instMul	—	Nat.instAtLeastTwoHAddOfNat Complex.ofReal_sub Complex.ofReal_div Complex.ofReal_pow Complex.sin_bound Complex.norm_real
sin_le_one 📖	mathematical	—	Real instLE sin instOne	—	abs_le instIsOrderedAddMonoid abs_sin_le_one
sin_neg 📖	mathematical	—	sin Real instNeg	—	Complex.ofReal_neg Complex.sin_neg
sin_pos_of_pos_of_le_one 📖	mathematical	Real instLT instZero instLE instOne	sin	—	Nat.instAtLeastTwoHAddOfNat sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid lt_sub_iff_add_lt add_le_add mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono instIsOrderedRing pow_le_pow_of_le_one IsOrderedRing.toPosMulMono abs_nonneg abs_of_nonneg le_of_lt pow_one div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_one Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toCharZero CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos CancelDenoms.sub_subst CancelDenoms.add_subst CancelDenoms.mul_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le sub_le_comm abs_sub_le_iff sin_bound
sin_pos_of_pos_of_le_two 📖	mathematical	Real instLT instZero instLE instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	sin	—	Nat.instAtLeastTwoHAddOfNat div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRing instIsOrderedRing instNontrivial one_mul mul_pos IsStrictOrderedRing.toPosMulStrictMono sin_pos_of_pos_of_le_one half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE cos_pos_of_le_one abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid le_of_lt sin_two_mul two_mul add_halves CharZero.NeZero.two IsStrictOrderedRing.toCharZero
sin_sq 📖	mathematical	—	Real Monoid.toNatPow instMonoid sin instSub instOne cos	—	eq_sub_iff_add_eq sin_sq_add_cos_sq
sin_sq_add_cos_sq 📖	mathematical	—	Real instAdd Monoid.toNatPow instMonoid sin cos instOne	—	Complex.ofReal_injective Complex.ofReal_add Complex.ofReal_pow Complex.ofReal_sin Complex.ofReal_cos Complex.sin_sq_add_cos_sq
sin_sq_eq_half_sub 📖	mathematical	—	Real Monoid.toNatPow instMonoid sin instSub DivInvMonoid.toDiv instDivInvMonoid instOne instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat cos instMul	—	Nat.instAtLeastTwoHAddOfNat sin_sq cos_sq sub_sub sub_half CharZero.NeZero.two IsStrictOrderedRing.toCharZero instIsStrictOrderedRing
sin_sq_le_one 📖	mathematical	—	Real instLE Monoid.toNatPow instMonoid sin instOne	—	sin_sq_add_cos_sq le_add_of_nonneg_right IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono instIsOrderedRing
sin_sub 📖	mathematical	—	sin Real instSub instMul cos	—	sub_eq_add_neg sin_add cos_neg sin_neg mul_neg
sin_sub_sin 📖	mathematical	—	Real instSub sin instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv instDivInvMonoid cos instAdd	—	Complex.ofReal_injective Nat.instAtLeastTwoHAddOfNat Complex.ofReal_sub Complex.ofReal_sin Complex.sin_sub_sin Complex.ofReal_mul Complex.ofReal_div Complex.ofReal_cos Complex.ofReal_add
sin_three_mul 📖	mathematical	—	sin Real instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instSub Monoid.toNatPow instMonoid	—	Nat.instAtLeastTwoHAddOfNat Complex.ofReal_sin Complex.ofReal_mul Complex.sin_three_mul Complex.ofReal_sub Complex.ofReal_pow
sin_two_mul 📖	mathematical	—	sin Real instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat cos	—	Complex.ofReal_injective Nat.instAtLeastTwoHAddOfNat Complex.ofReal_sin Complex.ofReal_mul Complex.sin_two_mul Complex.ofReal_cos
sin_zero 📖	mathematical	—	sin Real instZero	—	Complex.sin_zero
sinh_add 📖	mathematical	—	sinh Real instAdd instMul cosh	—	Complex.ofReal_sinh Complex.ofReal_add Complex.sinh_add Complex.ofReal_mul Complex.ofReal_cosh
sinh_add_cosh 📖	mathematical	—	Real instAdd sinh cosh exp	—	add_comm cosh_add_sinh
sinh_eq 📖	mathematical	—	sinh Real DivInvMonoid.toDiv instDivInvMonoid instSub exp instNeg instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Complex.ofReal_injective Nat.instAtLeastTwoHAddOfNat Complex.ofReal_sinh Complex.ofReal_div Complex.ofReal_sub Complex.ofReal_exp Complex.ofReal_neg
sinh_lt_cosh 📖	mathematical	—	Real instLT sinh cosh	—	lt_of_pow_lt_pow_left₀ IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing IsOrderedRing.toMulPosMono instIsOrderedRing LT.lt.le cosh_pos lt_add_one instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid cosh_sq
sinh_neg 📖	mathematical	—	sinh Real instNeg	—	Complex.ofReal_neg Complex.sinh_neg
sinh_sq 📖	mathematical	—	Real Monoid.toNatPow instMonoid sinh instSub cosh instOne	—	Complex.ofReal_pow Complex.ofReal_sinh Complex.sinh_sq Complex.ofReal_sub Complex.ofReal_cosh
sinh_sub 📖	mathematical	—	sinh Real instSub instMul cosh	—	sub_eq_add_neg sinh_add cosh_neg sinh_neg mul_neg
sinh_sub_cosh 📖	mathematical	—	Real instSub sinh cosh instNeg exp	—	neg_sub cosh_sub_sinh
sinh_three_mul 📖	mathematical	—	sinh Real instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instAdd Monoid.toNatPow instMonoid	—	Nat.instAtLeastTwoHAddOfNat Complex.ofReal_sinh Complex.ofReal_mul Complex.sinh_three_mul Complex.ofReal_add Complex.ofReal_pow
sinh_two_mul 📖	mathematical	—	sinh Real instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat cosh	—	Nat.instAtLeastTwoHAddOfNat Complex.ofReal_sinh Complex.ofReal_mul Complex.sinh_two_mul Complex.ofReal_cosh
sinh_zero 📖	mathematical	—	sinh Real instZero	—	Complex.sinh_zero
tan_div_sqrt_one_add_tan_sq 📖	mathematical	Real instLT instZero cos	DivInvMonoid.toDiv instDivInvMonoid tan sqrt instAdd instOne Monoid.toNatPow instMonoid sin	—	tan_mul_cos LT.lt.ne' inv_sqrt_one_add_tan_sq div_eq_mul_inv
tan_eq_sin_div_cos 📖	mathematical	—	tan Real DivInvMonoid.toDiv instDivInvMonoid sin cos	—	Complex.ofReal_injective Complex.ofReal_tan Complex.ofReal_div Complex.ofReal_sin Complex.ofReal_cos
tan_inv_eq_cot 📖	mathematical	—	Real instInv tan cot	—	Complex.ofReal_injective Complex.ofReal_inv Complex.ofReal_tan Complex.tan_inv_eq_cot Complex.ofReal_cot
tan_mul_cos 📖	mathematical	—	Real instMul tan cos sin	—	tan_eq_sin_div_cos div_mul_cancel₀
tan_neg 📖	mathematical	—	tan Real instNeg	—	Complex.ofReal_neg Complex.tan_neg
tan_sq_div_one_add_tan_sq 📖	mathematical	—	Real DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid tan instAdd instOne sin	—	div_eq_mul_inv tan_mul_cos mul_pow inv_one_add_tan_sq
tan_zero 📖	mathematical	—	tan Real instZero	—	Complex.tan_zero
tanh_eq 📖	mathematical	—	tanh Real DivInvMonoid.toDiv instDivInvMonoid instSub exp instNeg instAdd	—	tanh_eq_sinh_div_cosh Nat.instAtLeastTwoHAddOfNat sinh_eq cosh_eq div_div_div_cancel_right₀ two_ne_zero CharZero.NeZero.two IsStrictOrderedRing.toCharZero instIsStrictOrderedRing
tanh_eq_sinh_div_cosh 📖	mathematical	—	tanh Real DivInvMonoid.toDiv instDivInvMonoid sinh cosh	—	Complex.ofReal_tanh Complex.ofReal_div Complex.ofReal_sinh Complex.ofReal_cosh
tanh_lt_one 📖	mathematical	—	Real instLT tanh instOne	—	tanh_eq Mathlib.Tactic.FieldSimp.lt_eq_cancel_lt IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg LT.lt.ne' add_pos' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid exp_pos Mathlib.Tactic.FieldSimp.NF.cons_pos instZeroLEOneClass zero_lt_one NeZero.one GroupWithZero.toNontrivial
tanh_neg 📖	mathematical	—	tanh Real instNeg	—	Complex.ofReal_neg Complex.tanh_neg
tanh_sq_lt_one 📖	mathematical	—	Real instLT Monoid.toNatPow instMonoid tanh instOne	—	sq_lt_one_iff_abs_lt_one instIsStrictOrderedRing abs_tanh_lt_one
tanh_zero 📖	mathematical	—	tanh Real instZero	—	Complex.tanh_zero
two_mul_cos_mul_cos 📖	mathematical	—	Real instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat cos instAdd instSub	—	Nat.instAtLeastTwoHAddOfNat cos_sub cos_add add_add_sub_cancel Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add
two_mul_sin_mul_cos 📖	mathematical	—	Real instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat sin cos instAdd instSub	—	Nat.instAtLeastTwoHAddOfNat sin_sub sin_add sub_add_add_cancel Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add
two_mul_sin_mul_sin 📖	mathematical	—	Real instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat sin instSub cos instAdd	—	Nat.instAtLeastTwoHAddOfNat cos_sub cos_add add_sub_sub_cancel Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add

---

← Back to Index