Documentation Verification Report

Arctan

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

Statistics

Metric	Count
Definitions `arctan`	1
Theorems `arctan_tan`, `arg_one_add_mem_Ioo`, `cos_ne_zero_of_arctan_bounds`, `hasSum_arctan`, `hasSum_arctan_aux`, `ofReal_arctan`, `tan_arctan`, `hasSum_arctan`	8
Total	9

Complex

Definitions

Name	Category	Theorems
`arctan` 📖	CompOp	4 math math: `ofReal_arctan`, `arctan_tan`, `tan_arctan`, `hasSum_arctan`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arctan_tan` 📖	mathematical	`Real` `Real.instLT` `Real.instNeg` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `re` `Real.instLE`	`arctan` `tan`	—	`Nat.instAtLeastTwoHAddOfNat` `cos_ne_zero_of_arctan_bounds` `mul_div_mul_right` `add_mul` `Distrib.rightDistribClass` `sub_mul` `one_mul` `mul_rotate` `mul_div_cancel₀` `sub_eq_add_neg` `neg_mul` `sin_neg` `cos_neg` `exp_mul_I` `exp_sub` `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.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.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `log_exp` `MulZeroClass.zero_mul` `zero_add` `zero_sub` `mul_neg` `neg_zero` `add_zero` `div_lt_iff₀'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `two_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `neg_div` `le_div_iff₀'` `Mathlib.Tactic.Ring.div_congr` `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.IsRat.to_raw_eq` `Mathlib.Meta.NormNum.isRat_mul` `Mathlib.Meta.NormNum.IsInt.to_isRat` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsRat.to_isInt` `Mathlib.Meta.NormNum.IsRat.of_raw` `Mathlib.Meta.NormNum.IsRat.den_nz` `I_mul_I` `neg_neg`
`arg_one_add_mem_Ioo` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `Complex` `instNorm` `Real.instOne`	`Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `Real.instNeg` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `arg` `instAdd` `instOne`	—	`Nat.instAtLeastTwoHAddOfNat` `Set.mem_Ioo` `abs_lt` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `abs_arg_lt_pi_div_two_iff` `add_re` `one_re` `neg_lt_iff_pos_add'` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `LE.le.trans_lt` `abs_re_le_norm`
`cos_ne_zero_of_arctan_bounds` 📖	—	`Real` `Real.instLT` `Real.instNeg` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `re` `Real.instLE`	—	—	`Nat.instAtLeastTwoHAddOfNat` `cos_ne_zero_iff` `ext_iff` `not_and_or` `Nat.cast_one` `Int.cast_ofNat` `Int.cast_one` `Int.cast_add` `Int.cast_mul` `ofReal_add` `ofReal_mul` `Mathlib.Tactic.Contrapose.contrapose₄` `one_mul` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `mul_le_mul_iff_of_pos_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.pi_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `mul_div_assoc` `mul_lt_mul_iff_of_pos_right` `MulPosReflectLE.toMulPosReflectLT` `neg_eq_neg_one_mul`
`hasSum_arctan` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `Complex` `instNorm` `Real.instOne`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instNeg` `instOne` `instNatCast` `arctan` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `HasSum.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `HasSum.add` `IsTopologicalSemiring.toContinuousAdd` `hasSum_taylorSeries_log` `norm_mul` `norm_I` `mul_one` `hasSum_taylorSeries_neg_log` `Equiv.hasSum_iff` `hasSum_arctan_aux` `Distrib.rightDistribClass` `HasSum.prod_fiberwise` `TopologicalSpace.PseudoMetrizableSpace.regularSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `mul_comm` `Fin.sum_univ_two` `Odd.neg_one_pow` `add_zero` `neg_add_cancel` `MulZeroClass.zero_mul` `zero_div` `MulZeroClass.mul_zero` `zero_add` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `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.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Even.neg_one_pow` `mul_div_assoc` `mul_assoc` `Mathlib.Tactic.Ring.div_congr` `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.Tactic.Ring.neg_zero` `Mathlib.Meta.NormNum.instAtLeastTwo` `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.Tactic.Ring.mul_pf_left` `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.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Nat.cast_one` `Mathlib.Meta.NormNum.IsRat.to_isInt` `Mathlib.Meta.NormNum.IsRat.of_raw` `Mathlib.Meta.NormNum.IsRat.den_nz` `mul_pow` `pow_succ'` `pow_mul` `I_sq` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_one_cast` `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.pow_prod_atom` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `I_mul_I` `neg_neg` `one_mul` `hasSum_fintype` `SummationFilter.instLeAtTopUnconditional`
`hasSum_arctan_aux` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `Complex` `instNorm` `Real.instOne`	`instAdd` `log` `instOne` `instMul` `I` `instNeg` `instSub` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`mem_slitPlane_iff_arg` `mem_slitPlane_of_norm_lt_one` `norm_mul` `norm_I` `mul_one` `norm_neg` `log_inv` `sub_eq_add_neg` `log_mul_eq_add_log_iff` `Iff.ne` `inv_eq_zero` `Nat.instAtLeastTwoHAddOfNat` `arg_one_add_mem_Ioo` `arg_inv` `Real.instIsOrderedAddMonoid` `neg_neg` `add_lt_add` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `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.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.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.IsRat.to_isInt` `Mathlib.Meta.NormNum.isRat_add` `Mathlib.Meta.NormNum.IsRat.of_raw` `Mathlib.Meta.NormNum.IsRat.den_nz` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsNat.to_isInt` `LT.lt.le` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_add` `div_eq_mul_inv`
`ofReal_arctan` 📖	mathematical	—	`ofReal` `Real.arctan` `arctan`	—	`Real.tan_arctan` `ofReal_tan` `arctan_tan` `Nat.instAtLeastTwoHAddOfNat` `LT.lt.ne` `Real.arctan_lt_pi_div_two` `Real.neg_pi_div_two_lt_arctan` `LT.lt.le`
`tan_arctan` 📖	mathematical	—	`tan` `arctan`	—	`div_div_eq_mul_div` `div_mul_cancel₀` `two_ne_zero` `CharZero.NeZero.two` `instCharZero` `div_mul_eq_mul_div` `mul_div_mul_right` `exp_ne_zero` `sub_mul` `add_mul` `Distrib.rightDistribClass` `exp_add` `neg_mul` `neg_add_cancel` `exp_zero` `Nat.instAtLeastTwoHAddOfNat` `two_mul` `Mathlib.Tactic.Contrapose.contrapose₄` `neg_neg` `neg_one_mul` `div_I` `div_eq_iff` `I_ne_zero` `add_eq_zero_iff_neg_eq` `one_mul` `sub_eq_zero` `arctan.eq_1` `mul_rotate` `mul_assoc` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `neg_div` `mul_neg` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `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.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Meta.NormNum.isNat_eq_false` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_zero` `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.one_eq_eval` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `I_sq` `exp_log` `div_ne_zero` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `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.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `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_overlap_pf_zero` `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.IsRat.to_isInt` `Mathlib.Meta.NormNum.isRat_mul` `Mathlib.Meta.NormNum.IsInt.to_isRat` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.neg_congr` `I_mul_I`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasSum_arctan` 📖	mathematical	`Real` `instLT` `Norm.norm` `norm` `instOne`	`HasSum` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul` `Monoid.toNatPow` `instMonoid` `instNeg` `instNatCast` `arctan` `SummationFilter.unconditional`	—	`Nat.cast_one` `Int.cast_pow` `Int.cast_neg` `Int.cast_one` `Complex.ofReal_pow` `Complex.ofReal_neg` `Nat.instAtLeastTwoHAddOfNat` `Nat.cast_add` `Nat.cast_mul` `Complex.ofReal_add` `Complex.ofReal_mul` `Complex.hasSum_arctan` `Complex.norm_real`

---

← Back to Index