Complex

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

Statistics

Metric	Count
Definitions	0
Theorems continuousOn_tan, continuous_tan, cos_eq_cos_iff, cos_eq_iff_quadratic, cos_eq_neg_one_iff, cos_eq_one_iff, cos_eq_two_mul_tan_half_div_one_sub_tan_half_sq, cos_eq_zero_iff, cos_ne_zero_iff, cos_surjective, range_cos, range_sin, sin_eq_neg_one_iff, sin_eq_one_iff, sin_eq_sin_iff, sin_eq_two_mul_tan_half_div_one_add_tan_half_sq, sin_eq_zero_iff, sin_ne_zero_iff, sin_surjective, tan_add, tan_add', tan_add_mul_I, tan_eq, tan_eq_one_sub_tan_half_sq_div_one_add_tan_half_sq, tan_eq_zero_iff, tan_eq_zero_iff', tan_eq_zero_of_cos_eq_zero, tan_int_mul_pi_div_two, tan_ne_zero_iff, tan_sub, tan_sub', tan_two_mul, abs_cos_eq_one_iff, abs_sin_eq_one_iff, cos_eq_cos_iff, cos_eq_neg_one_iff, cos_eq_two_mul_tan_half_div_one_sub_tan_half_sq, cos_eq_zero_iff, cos_ne_zero_iff, sin_eq_neg_one_iff, sin_eq_one_iff, sin_eq_sin_iff, sin_eq_two_mul_tan_half_div_one_add_tan_half_sq, tan_eq_one_sub_tan_half_sq_div_one_add_tan_half_sq, tan_eq_zero_iff, tan_eq_zero_iff', tan_eq_zero_of_cos_eq_zero, tan_ne_zero_iff	48
Total	48

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_tan 📖	mathematical	—	ContinuousOn Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField tan setOf cos instZero	—	ContinuousOn.div IsTopologicalDivisionRing.toContinuousInv₀ NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing continuousOn_sin continuousOn_cos
continuous_tan 📖	mathematical	—	Continuous Set.Elem Complex setOf cos instZero instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField tan	—	continuousOn_iff_continuous_restrict continuousOn_tan
cos_eq_cos_iff 📖	mathematical	—	cos Complex instAdd instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instIntCast ofReal Real.pi instSub	—	Nat.instAtLeastTwoHAddOfNat sub_eq_zero cos_sub_cos neg_mul NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass instCharZero Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero 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.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial mul_comm mul_right_comm Mathlib.Tactic.FieldSimp.subst_add Int.cast_neg neg_add_cancel_left
cos_eq_iff_quadratic 📖	mathematical	—	cos Complex instAdd instSub Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring exp instMul I instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instOne instZero	—	Nat.instAtLeastTwoHAddOfNat sub_eq_zero neg_mul exp_neg Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ 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.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.zpow'_one 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.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial MulZeroClass.mul_zero Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos 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 Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_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.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.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add
cos_eq_neg_one_iff 📖	mathematical	—	cos Complex instNeg instOne instAdd ofReal Real.pi instMul instIntCast instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat neg_eq_iff_eq_neg cos_sub_pi cos_eq_one_iff
cos_eq_one_iff 📖	mathematical	—	cos Complex instOne instMul instIntCast instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat ofReal Real.pi	—	Nat.instAtLeastTwoHAddOfNat cos_zero cos_eq_cos_iff mul_assoc mul_left_comm add_zero sub_zero
cos_eq_two_mul_tan_half_div_one_sub_tan_half_sq 📖	mathematical	—	cos Complex DivInvMonoid.toDiv instDivInvMonoid instSub instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring tan instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instAdd	—	Nat.instAtLeastTwoHAddOfNat mul_div_cancel₀ two_ne_zero CharZero.NeZero.two instCharZero cos_two_mul' div_eq_mul_inv inv_one_add_tan_sq tan_mul_cos Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr 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.mul_congr Mathlib.Tactic.Ring.mul_pf_right 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 Nat.cast_one Mathlib.Tactic.Ring.mul_one
cos_eq_zero_iff 📖	mathematical	—	cos Complex instZero DivInvMonoid.toDiv instDivInvMonoid instMul instAdd instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instIntCast instOne ofReal Real.pi	—	Nat.instAtLeastTwoHAddOfNat div_eq_iff two_ne_zero CharZero.NeZero.two instCharZero MulZeroClass.zero_mul add_eq_zero_iff_eq_neg neg_eq_neg_one_mul exp_ne_zero exp_sub 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.neg_congr 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.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo cos.eq_1 exp_pi_mul_I exp_eq_exp_iff_exists_int mul_right_comm Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.div_congr Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz mul_right_inj' IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass I_ne_zero
cos_ne_zero_iff 📖	—	—	—	—	Mathlib.Tactic.Contrapose.contrapose_iff₂ Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Push.not_forall_eq cos_eq_zero_iff
cos_surjective 📖	mathematical	—	Complex cos	—	Nat.instAtLeastTwoHAddOfNat exists_quadratic_eq_zero CharZero.NeZero.two instCharZero one_ne_zero NeZero.charZero_one cpow_nat_inv_pow two_ne_zero pow_two MulZeroClass.mul_zero zero_add cos_eq_iff_quadratic div_mul_cancel₀ I_ne_zero exp_log Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr 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.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_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.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Nat.cast_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.neg_congr
range_cos 📖	mathematical	—	Set.range Complex cos Set.univ	—	Function.Surjective.range_eq cos_surjective
range_sin 📖	mathematical	—	Set.range Complex sin Set.univ	—	Function.Surjective.range_eq sin_surjective
sin_eq_neg_one_iff 📖	mathematical	—	sin Complex instNeg instOne instAdd DivInvMonoid.toDiv instDivInvMonoid ofReal Real.pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instMul instIntCast	—	Nat.instAtLeastTwoHAddOfNat neg_eq_iff_eq_neg cos_add_pi_div_two cos_eq_one_iff
sin_eq_one_iff 📖	mathematical	—	sin Complex instOne instAdd DivInvMonoid.toDiv instDivInvMonoid ofReal Real.pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instMul instIntCast	—	Nat.instAtLeastTwoHAddOfNat cos_sub_pi_div_two cos_eq_one_iff
sin_eq_sin_iff 📖	mathematical	—	sin Complex instAdd instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instIntCast ofReal Real.pi instSub instOne	—	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.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ 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.zpow'_one Mathlib.Tactic.FieldSimp.subst_sub 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.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add 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.atom_pf Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_pf_left 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 Mathlib.Tactic.Ring.add_pf_zero_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.Meta.NormNum.isNat_mul Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Nat.cast_one Mathlib.Tactic.Ring.one_mul
sin_eq_two_mul_tan_half_div_one_add_tan_half_sq 📖	mathematical	—	sin Complex DivInvMonoid.toDiv instDivInvMonoid instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat tan instAdd instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring	—	Nat.instAtLeastTwoHAddOfNat mul_div_cancel₀ two_ne_zero CharZero.NeZero.two instCharZero sin_two_mul MulZeroClass.mul_zero tan_eq_zero_of_cos_eq_zero zero_pow Nat.instCharZero add_zero div_one div_eq_mul_inv inv_one_add_tan_sq tan_mul_cos 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_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_one 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.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
sin_eq_zero_iff 📖	mathematical	—	sin Complex instZero instMul instIntCast ofReal Real.pi	—	Nat.instAtLeastTwoHAddOfNat cos_sub_pi_div_two cos_eq_zero_iff eq_add_of_sub_eq Int.cast_add Int.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.div_congr 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 Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNNRat_add Int.cast_sub 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.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isInt_add
sin_ne_zero_iff 📖	—	—	—	—	Mathlib.Tactic.Contrapose.contrapose_iff₂ Mathlib.Tactic.Push.not_forall_eq sin_eq_zero_iff
sin_surjective 📖	mathematical	—	Complex sin	—	cos_surjective Nat.instAtLeastTwoHAddOfNat sin_add_pi_div_two
tan_add 📖	mathematical	Complex DivInvMonoid.toDiv instDivInvMonoid instMul instAdd instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instIntCast instOne ofReal Real.pi	tan instSub	—	Nat.instAtLeastTwoHAddOfNat tan.eq_1 sin_add cos_add div_div_div_cancel_right₀ mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass cos_ne_zero_iff add_div sub_div div_self mul_one one_mul Int.cast_add Int.cast_mul Int.cast_two Int.cast_one tan_int_mul_pi_div_two add_zero zero_div mul_div_assoc add_mul Distrib.rightDistribClass
tan_add' 📖	mathematical	—	tan Complex instAdd DivInvMonoid.toDiv instDivInvMonoid instSub instOne instMul	—	Nat.instAtLeastTwoHAddOfNat tan_add
tan_add_mul_I 📖	mathematical	Complex DivInvMonoid.toDiv instDivInvMonoid instMul instAdd instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instIntCast instOne ofReal Real.pi I	tan tanh instSub	—	Nat.instAtLeastTwoHAddOfNat tan_add tan_mul_I mul_assoc
tan_eq 📖	mathematical	ofReal re Complex DivInvMonoid.toDiv instDivInvMonoid instMul instAdd instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instIntCast instOne Real.pi im I	tan tanh instSub	—	Nat.instAtLeastTwoHAddOfNat re_add_im tan_add_mul_I
tan_eq_one_sub_tan_half_sq_div_one_add_tan_half_sq 📖	mathematical	—	tan Complex DivInvMonoid.toDiv instDivInvMonoid instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instSub instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring	—	Nat.instAtLeastTwoHAddOfNat mul_div_cancel₀ two_ne_zero CharZero.NeZero.two instCharZero tan_two_mul
tan_eq_zero_iff 📖	mathematical	—	tan Complex instZero DivInvMonoid.toDiv instDivInvMonoid instMul instIntCast ofReal Real.pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat tan.eq_1 div_eq_zero_iff mul_eq_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass mul_right_inj' IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain two_ne_zero CharZero.NeZero.two instCharZero MulZeroClass.mul_zero mul_assoc sin_two_mul sin_eq_zero_iff mul_comm Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one 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 one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero 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.NF.cons_ne_zero
tan_eq_zero_iff' 📖	mathematical	—	tan Complex instZero instMul instIntCast ofReal Real.pi	—	—
tan_eq_zero_of_cos_eq_zero 📖	mathematical	cos Complex instZero	tan	—	Nat.instAtLeastTwoHAddOfNat cos_eq_zero_iff tan_eq_zero_iff Int.cast_add Int.cast_mul Int.cast_ofNat Int.cast_one
tan_int_mul_pi_div_two 📖	mathematical	—	tan Complex DivInvMonoid.toDiv instDivInvMonoid instMul instIntCast ofReal Real.pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instZero	—	Nat.instAtLeastTwoHAddOfNat tan_eq_zero_iff
tan_ne_zero_iff 📖	—	—	—	—	Mathlib.Tactic.Contrapose.contrapose_iff₂ Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Push.not_forall_eq tan_eq_zero_iff
tan_sub 📖	mathematical	Complex DivInvMonoid.toDiv instDivInvMonoid instMul instAdd instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instIntCast instOne ofReal Real.pi	tan instSub	—	Nat.instAtLeastTwoHAddOfNat tan_add neg_eq_iff_eq_neg Int.cast_sub Int.cast_neg Int.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_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 Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.IsInt.to_isNat tan_neg
tan_sub' 📖	mathematical	—	tan Complex instSub DivInvMonoid.toDiv instDivInvMonoid instAdd instOne instMul	—	Nat.instAtLeastTwoHAddOfNat tan_sub
tan_two_mul 📖	mathematical	—	tan Complex instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv instDivInvMonoid instSub instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring	—	Nat.instAtLeastTwoHAddOfNat two_mul sq tan_add Mathlib.Tactic.Push.not_forall_eq

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_cos_eq_one_iff 📖	mathematical	—	abs Real lattice instAddGroup cos instOne instMul instIntCast pi	—	abs_one instIsOrderedRing abs_eq_abs Nat.instAtLeastTwoHAddOfNat cos_eq_one_iff cos_eq_neg_one_iff Int.even_or_odd
abs_sin_eq_one_iff 📖	mathematical	—	abs Real lattice instAddGroup sin instOne instAdd DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instMul instIntCast	—	Nat.instAtLeastTwoHAddOfNat abs_one instIsOrderedRing abs_eq_abs sin_eq_one_iff sin_eq_neg_one_iff Int.even_or_odd
cos_eq_cos_iff 📖	mathematical	—	cos Real instAdd instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instIntCast pi instSub	—	Nat.instAtLeastTwoHAddOfNat Int.cast_ofNat Int.cast_mul Complex.ofReal_mul Complex.cos_eq_cos_iff
cos_eq_neg_one_iff 📖	mathematical	—	cos Real instNeg instOne instAdd pi instMul instIntCast instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.cast_one Int.cast_neg Int.cast_one Complex.ofReal_neg Complex.cos_eq_neg_one_iff
cos_eq_two_mul_tan_half_div_one_sub_tan_half_sq 📖	mathematical	—	cos Real DivInvMonoid.toDiv instDivInvMonoid instSub instOne Monoid.toNatPow instMonoid tan instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instAdd	—	Nat.instAtLeastTwoHAddOfNat Nat.cast_one Complex.cos_eq_two_mul_tan_half_div_one_sub_tan_half_sq Int.cast_neg Int.cast_one Complex.ofReal_neg
cos_eq_zero_iff 📖	mathematical	—	cos Real instZero DivInvMonoid.toDiv instDivInvMonoid instMul instAdd instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instIntCast instOne pi	—	Nat.instAtLeastTwoHAddOfNat Nat.cast_zero Nat.cast_one Int.cast_ofNat Int.cast_one Int.cast_add Int.cast_mul Complex.ofReal_add Complex.ofReal_mul Complex.cos_eq_zero_iff
cos_ne_zero_iff 📖	—	—	—	—	Nat.instAtLeastTwoHAddOfNat Nat.cast_zero Nat.cast_one Int.cast_ofNat Int.cast_one Int.cast_add Int.cast_mul Complex.ofReal_add Complex.ofReal_mul Complex.cos_ne_zero_iff
sin_eq_neg_one_iff 📖	mathematical	—	sin Real instNeg instOne instAdd DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instMul instIntCast	—	Nat.cast_one Int.cast_neg Int.cast_one Complex.ofReal_neg Complex.sin_eq_neg_one_iff
sin_eq_one_iff 📖	mathematical	—	sin Real instOne instAdd DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instMul instIntCast	—	Nat.instAtLeastTwoHAddOfNat Nat.cast_one Complex.sin_eq_one_iff
sin_eq_sin_iff 📖	mathematical	—	sin Real instAdd instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instIntCast pi instSub instOne	—	Nat.instAtLeastTwoHAddOfNat Nat.cast_one Int.cast_ofNat Int.cast_mul Complex.ofReal_mul Int.cast_one Int.cast_add Complex.ofReal_add Complex.sin_eq_sin_iff
sin_eq_two_mul_tan_half_div_one_add_tan_half_sq 📖	mathematical	—	sin Real DivInvMonoid.toDiv instDivInvMonoid instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat tan instAdd instOne Monoid.toNatPow instMonoid	—	Nat.instAtLeastTwoHAddOfNat Nat.cast_one Complex.sin_eq_two_mul_tan_half_div_one_add_tan_half_sq
tan_eq_one_sub_tan_half_sq_div_one_add_tan_half_sq 📖	mathematical	—	tan Real DivInvMonoid.toDiv instDivInvMonoid instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instSub instOne Monoid.toNatPow instMonoid	—	Nat.instAtLeastTwoHAddOfNat Nat.cast_one Complex.tan_eq_one_sub_tan_half_sq_div_one_add_tan_half_sq
tan_eq_zero_iff 📖	mathematical	—	tan Real instZero DivInvMonoid.toDiv instDivInvMonoid instMul instIntCast pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Nat.cast_zero Complex.tan_eq_zero_iff
tan_eq_zero_iff' 📖	mathematical	—	tan Real instZero instMul instIntCast pi	—	Nat.cast_zero Complex.tan_eq_zero_iff'
tan_eq_zero_of_cos_eq_zero 📖	mathematical	cos Real instZero	tan	—	Nat.cast_zero Complex.tan_eq_zero_of_cos_eq_zero
tan_ne_zero_iff 📖	—	—	—	—	Nat.instAtLeastTwoHAddOfNat Nat.cast_zero Complex.tan_ne_zero_iff

---

← Back to Index