Arg

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

Statistics

Metric	Count
Definitions arg, Arg	2
Theorems abs_arg_inv, abs_arg_le_pi, abs_arg_le_pi_div_two_iff, abs_arg_lt_pi_div_two_iff, arg_I, arg_coe_angle_eq_iff, arg_coe_angle_eq_iff_eq_toReal, arg_coe_angle_toReal_eq_arg, arg_conj, arg_conj_coe_angle, arg_cos_add_sin_mul_I, arg_cos_add_sin_mul_I_coe_angle, arg_cos_add_sin_mul_I_eq_toIocMod, arg_cos_add_sin_mul_I_sub, arg_div_coe_angle, arg_div_self, arg_eq_arg_iff, arg_eq_neg_pi_div_two_iff, arg_eq_nhds_of_im_neg, arg_eq_nhds_of_im_pos, arg_eq_nhds_of_re_neg_of_im_neg, arg_eq_nhds_of_re_neg_of_im_pos, arg_eq_nhds_of_re_pos, arg_eq_pi_div_two_iff, arg_eq_pi_iff, arg_eq_pi_iff_lt_zero, arg_eq_zero_iff, arg_eq_zero_iff_zero_le, arg_exp, arg_exp_mul_I, arg_inv, arg_inv_coe_angle, arg_le_pi, arg_le_pi_div_two_iff, arg_lt_pi_div_two_iff, arg_lt_pi_iff, arg_mem_Ioc, arg_mul, arg_mul_coe_angle, arg_mul_cos_add_sin_mul_I, arg_mul_cos_add_sin_mul_I_coe_angle, arg_mul_cos_add_sin_mul_I_eq_toIocMod, arg_mul_cos_add_sin_mul_I_sub, arg_mul_eq_add_arg_iff, arg_mul_real, arg_neg_I, arg_neg_coe_angle, arg_neg_eq_arg_add_pi_iff, arg_neg_eq_arg_add_pi_of_im_neg, arg_neg_eq_arg_sub_pi_iff, arg_neg_eq_arg_sub_pi_of_im_pos, arg_neg_iff, arg_neg_one, arg_nonneg_iff, arg_ofReal_of_neg, arg_ofReal_of_nonneg, arg_of_im_neg, arg_of_im_nonneg_of_ne_zero, arg_of_im_pos, arg_of_re_neg_of_im_neg, arg_of_re_neg_of_im_nonneg, arg_of_re_nonneg, arg_one, arg_pow_coe_angle, arg_real_mul, arg_zero, arg_zpow_coe_angle, continuousAt_arg, continuousAt_arg_coe_angle, continuousOn_arg, continuousWithinAt_arg_of_re_neg_of_im_zero, cos_arg, exp_mem_slitPlane, ext_norm_arg, ext_norm_arg_iff, image_exp_Ioc_eq_sphere, mem_slitPlane_iff_arg, natCast_arg, neg_pi_div_two_le_arg_iff, neg_pi_div_two_lt_arg_iff, neg_pi_lt_arg, norm_eq_one_iff, norm_eq_one_iff', norm_mul_cos_add_sin_mul_I, norm_mul_cos_arg, norm_mul_exp_arg_mul_I, norm_mul_sin_arg, ofNat_arg, range_arg, range_exp_mul_I, sin_arg, slitPlane_arg_ne_pi, tan_arg, tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero, tendsto_arg_nhdsWithin_im_nonneg_of_re_neg_of_im_zero, toIocMod_arg	96
Total	98

Complex

Definitions

Name	Category	Theorems
arg 📖	CompOp	131 math math: log_conj_eq_ite, isTheta_exp_arg_mul_im, Circle.exp_arg, Circle.injective_arg, continuousWithinAt_arg_of_re_neg_of_im_zero, arg_neg_I, arg_cos_add_sin_mul_I_coe_angle, measurable_arg, arg_div_self, continuousOn_arg, arg_of_re_nonneg, arg_coe_angle_eq_iff, oangle, arg_le_pi, AddCircle.homeomorphCircle'_symm_apply, arg_one, neg_pi_div_two_lt_arg_iff, arg_mul_eq_add_arg_iff, arg_le_pi_div_two_iff, log_inv_eq_ite, continuousAt_arg, tan_arg, arg_cos_add_sin_mul_I, arg_of_re_neg_of_im_nonneg, ofNat_arg, arg_coe_angle_eq_iff_eq_toReal, arg_of_im_pos, arg_neg_eq_arg_sub_pi_of_im_pos, arg_ofReal_of_nonneg, Circle.arg_eq_arg, arg_mul_cos_add_sin_mul_I_eq_toIocMod, arg_cos_add_sin_mul_I_sub, norm_cpow_of_ne_zero, norm_mul_cos_arg, norm_cpow_of_imp, abs_arg_le_pi, arg_mul_cos_add_sin_mul_I, polarCoord_apply, cpow_ofReal_re, norm_add_eq_iff, tendsto_arg_nhdsWithin_im_nonneg_of_re_neg_of_im_zero, arg_neg_eq_arg_add_pi_iff, inv_cpow_eq_ite', arg_one_add_mem_Ioo, arg_exp_mul_I, arg_of_re_neg_of_im_neg, IsSelfAdjoint.cfc_arg, arg_lt_pi_div_two_iff, arg_mul_cos_add_sin_mul_I_coe_angle, arg_mem_Ioc, tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero, Real.Angle.arg_toCircle, arg_eq_zero_iff_zero_le, angle_eq_abs_arg, arg_zero, neg_pi_lt_arg, inv_cpow_eq_ite, Circle.invOn_arg_exp, arg_neg_eq_arg_add_pi_of_im_neg, arg_conj, arg_eq_nhds_of_im_neg, IsPrimitiveRoot.arg_eq_zero_iff, arg_lt_pi_iff, arg_of_im_nonneg_of_ne_zero, arg_eq_pi_div_two_iff, range_arg, log_mul_eq_add_log_iff, conj_cpow_eq_ite, norm_mul_cos_add_sin_mul_I, abs_arg_inv, Circle.leftInverse_exp_arg, norm_mul_exp_arg_mul_I, abs_arg_le_pi_div_two_iff, arg_eq_arg_iff, continuousAt_arg_coe_angle, arg_div_coe_angle, AEMeasurable.carg, log_im, arg_neg_one, arg_neg_iff, toIocMod_arg, arg_of_im_neg, arg_eq_zero_iff, abs_arg_lt_pi_div_two_iff, ext_norm_arg_iff, arg_conj_coe_angle, arg_mul_real, arg_inv, norm_sub_eq_iff, cpow_ofReal_im, arg_coe_angle_toReal_eq_arg, polarCoord_apply, sameRay_iff, sameRay_iff_arg_div_eq_zero, arg_eq_nhds_of_im_pos, arg_real_mul, angle_one_left, neg_pi_div_two_le_arg_iff, angle_one_right, arg_eq_nhds_of_re_pos, arg_pow_coe_angle, arg_ofReal_of_neg, Circle.arg_exp, arg_eq_nhds_of_re_neg_of_im_pos, arg_nonneg_iff, arg_inv_coe_angle, arg_exp, IsPrimitiveRoot.arg, Orientation.oangle_map_complex, natCast_arg, norm_cpow_le, arg_eq_nhds_of_re_neg_of_im_neg, arg_mul_cos_add_sin_mul_I_sub, Unitary.argSelfAdjoint_coe, arg_mul_coe_angle, Measurable.carg, arg_neg_eq_arg_sub_pi_iff, arg_I, arg_eq_pi_iff, arg_zpow_coe_angle, arg_cos_add_sin_mul_I_eq_toIocMod, Circle.argEquiv_apply_coe, sin_arg, IsPrimitiveRoot.arg_eq_pi_iff, cos_arg, arg_eq_neg_pi_div_two_iff, Circle.argPartialEquiv_apply, arg_eq_pi_iff_lt_zero, cpow_ofReal, norm_mul_sin_arg, arg_neg_coe_angle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_arg_inv 📖	mathematical	—	abs Real Real.lattice Real.instAddGroup arg Complex instInv	—	arg_inv abs_neg
abs_arg_le_pi 📖	mathematical	—	Real Real.instLE abs Real.lattice Real.instAddGroup arg Real.pi	—	abs_le Real.instIsOrderedAddMonoid LT.lt.le neg_pi_lt_arg arg_le_pi
abs_arg_le_pi_div_two_iff 📖	mathematical	—	Real Real.instLE abs Real.lattice Real.instAddGroup arg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instZero re	—	Nat.instAtLeastTwoHAddOfNat abs_le Real.instIsOrderedAddMonoid arg_le_pi_div_two_iff neg_pi_div_two_le_arg_iff not_le
abs_arg_lt_pi_div_two_iff 📖	mathematical	—	Real Real.instLT abs Real.lattice Real.instAddGroup arg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instZero re Complex instZero	—	Nat.instAtLeastTwoHAddOfNat abs_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add arg_lt_pi_div_two_iff neg_pi_div_two_lt_arg_iff eq_or_ne
arg_I 📖	mathematical	—	arg I Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat norm_I div_self NeZero.charZero_one RCLike.charZero_rclike Real.arcsin_one
arg_coe_angle_eq_iff 📖	mathematical	—	Real.Angle.coe arg	—	arg_coe_angle_toReal_eq_arg
arg_coe_angle_eq_iff_eq_toReal 📖	mathematical	—	Real.Angle.coe arg Real.Angle.toReal	—	arg_coe_angle_toReal_eq_arg
arg_coe_angle_toReal_eq_arg 📖	mathematical	—	Real.Angle.toReal Real.Angle.coe arg	—	Real.Angle.toReal_coe_eq_self_iff_mem_Ioc arg_mem_Ioc
arg_conj 📖	mathematical	—	arg DFunLike.coe RingHom Complex Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing Real Real.pi Real.decidableEq Real.instNeg	—	norm_conj neg_div neg_neg Real.arcsin_neg lt_trichotomy LT.lt.not_ge IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.le add_comm LT.lt.ne not_le neg_sub sub_neg_eq_add neg_zero zero_div Real.arcsin_zero zero_add sub_eq_neg_add neg_add_rev LE.le.not_gt
arg_conj_coe_angle 📖	mathematical	—	Real.Angle.coe arg DFunLike.coe RingHom Complex Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing Real.Angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	arg_conj Real.Angle.neg_coe_pi
arg_cos_add_sin_mul_I 📖	mathematical	Real Set Set.instMembership Set.Ioc Real.instPreorder Real.instNeg Real.pi	arg Complex instAdd cos ofReal instMul sin I	—	one_mul ofReal_one arg_mul_cos_add_sin_mul_I zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
arg_cos_add_sin_mul_I_coe_angle 📖	mathematical	—	Real.Angle.coe arg Complex instAdd ofReal Real.Angle.cos instMul Real.Angle.sin I	—	one_mul ofReal_one arg_mul_cos_add_sin_mul_I_coe_angle zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
arg_cos_add_sin_mul_I_eq_toIocMod 📖	mathematical	—	arg Complex instAdd cos ofReal instMul sin I toIocMod Real Real.instAddCommGroup Real.linearOrder Real.instIsOrderedAddMonoid Real.instArchimedean Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Real.two_pi_pos Real.instNeg	—	Real.instIsOrderedAddMonoid Real.instArchimedean Nat.instAtLeastTwoHAddOfNat Real.two_pi_pos one_mul ofReal_one arg_mul_cos_add_sin_mul_I_eq_toIocMod zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
arg_cos_add_sin_mul_I_sub 📖	mathematical	—	Real Real.instSub arg Complex instAdd cos ofReal instMul sin I Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Real.instIntCast Int.floor Real.instRing Real.linearOrder Real.instFloorRing DivInvMonoid.toDiv Real.instDivInvMonoid	—	Nat.instAtLeastTwoHAddOfNat one_mul ofReal_one arg_mul_cos_add_sin_mul_I_sub zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
arg_div_coe_angle 📖	mathematical	—	Real.Angle.coe arg Complex DivInvMonoid.toDiv instDivInvMonoid Real.Angle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle	—	div_eq_mul_inv arg_mul_coe_angle inv_ne_zero arg_inv_coe_angle sub_eq_add_neg
arg_div_self 📖	mathematical	—	arg Complex DivInvMonoid.toDiv instDivInvMonoid Real Real.instZero	—	eq_or_ne div_zero arg_zero div_self arg_one
arg_eq_arg_iff 📖	mathematical	—	arg Complex instMul DivInvMonoid.toDiv instDivInvMonoid ofReal Norm.norm instNorm	—	norm_mul NormedDivisionRing.toNormMulClass norm_div norm_real norm_norm div_mul_cancel₀ norm_ne_zero_iff ofReal_div arg_real_mul div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing norm_pos_iff
arg_eq_neg_pi_div_two_iff 📖	mathematical	—	arg Real Real.instNeg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat re Real.instZero Real.instLT im	—	Nat.instAtLeastTwoHAddOfNat arg_zero RCLike.charZero_rclike norm_mul_cos_add_sin_mul_I ofReal_neg ofReal_div cos_neg cos_pi_div_two sin_neg sin_pi_div_two neg_mul one_mul zero_add mul_neg MulZeroClass.mul_zero mul_one sub_self neg_zero add_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid arg_neg_I arg_real_mul neg_pos mk_eq_add_mul_I neg_neg
arg_eq_nhds_of_im_neg 📖	mathematical	Real Real.instLT im Real.instZero	Filter.EventuallyEq Complex nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField arg Real.instNeg Real.arccos DivInvMonoid.toDiv Real.instDivInvMonoid re Norm.norm instNorm	—	Filter.Eventually.mono Filter.Tendsto.eventually Continuous.tendsto continuous_im gt_mem_nhds instOrderTopologyReal arg_of_im_neg
arg_eq_nhds_of_im_pos 📖	mathematical	Real Real.instLT Real.instZero im	Filter.EventuallyEq Complex nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField arg Real.arccos DivInvMonoid.toDiv Real.instDivInvMonoid re Norm.norm instNorm	—	Filter.Eventually.mono Filter.Tendsto.eventually Continuous.tendsto continuous_im lt_mem_nhds instOrderTopologyReal arg_of_im_pos
arg_eq_nhds_of_re_neg_of_im_neg 📖	mathematical	Real Real.instLT re Real.instZero im	Filter.EventuallyEq Complex nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField arg Real.instSub Real.arcsin DivInvMonoid.toDiv Real.instDivInvMonoid instNeg Norm.norm instNorm Real.pi	—	IsOpen.eventually_mem IsOpen.and isOpen_lt HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid continuous_re continuous_zero continuous_im Filter.Eventually.mono arg_of_re_neg_of_im_neg
arg_eq_nhds_of_re_neg_of_im_pos 📖	mathematical	Real Real.instLT re Real.instZero im	Filter.EventuallyEq Complex nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField arg Real.instAdd Real.arcsin DivInvMonoid.toDiv Real.instDivInvMonoid instNeg Norm.norm instNorm Real.pi	—	IsOpen.eventually_mem IsOpen.and isOpen_lt HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid continuous_re continuous_zero continuous_im Filter.Eventually.mono arg_of_re_neg_of_im_nonneg LT.lt.le
arg_eq_nhds_of_re_pos 📖	mathematical	Real Real.instLT Real.instZero re	Filter.EventuallyEq Complex nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField arg Real.arcsin DivInvMonoid.toDiv Real.instDivInvMonoid im Norm.norm instNorm	—	Filter.Eventually.mono Filter.Tendsto.eventually Continuous.tendsto continuous_re lt_mem_nhds instOrderTopologyReal arg_of_re_nonneg LT.lt.le
arg_eq_pi_div_two_iff 📖	mathematical	—	arg Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat re Real.instZero Real.instLT im	—	Nat.instAtLeastTwoHAddOfNat arg_zero LT.lt.ne Real.pi_div_two_pos norm_mul_cos_add_sin_mul_I ofReal_div cos_pi_div_two sin_pi_div_two one_mul zero_add MulZeroClass.mul_zero mul_one sub_self add_zero arg_I arg_real_mul ofReal_mul' I_re I_im
arg_eq_pi_iff 📖	mathematical	—	arg Real.pi Real Real.instLT re Real.instZero im	—	arg_zero Real.pi_ne_zero norm_mul_cos_add_sin_mul_I cos_pi sin_pi MulZeroClass.zero_mul add_zero mul_neg mul_one IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid neg_zero arg_neg_one arg_real_mul neg_pos ofReal_neg neg_neg
arg_eq_pi_iff_lt_zero 📖	mathematical	—	arg Real.pi Complex Preorder.toLT PartialOrder.toPreorder partialOrder instZero	—	arg_eq_pi_iff
arg_eq_zero_iff 📖	mathematical	—	arg Real Real.instZero Real.instLE re im	—	norm_mul_cos_add_sin_mul_I cos_zero sin_zero MulZeroClass.zero_mul add_zero mul_one arg_ofReal_of_nonneg
arg_eq_zero_iff_zero_le 📖	mathematical	—	arg Real Real.instZero Complex Preorder.toLE PartialOrder.toPreorder partialOrder instZero	—	arg_eq_zero_iff nonneg_iff
arg_exp 📖	mathematical	—	arg exp toIocMod Real Real.instAddCommGroup Real.linearOrder Real.instIsOrderedAddMonoid Real.instArchimedean Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Real.two_pi_pos Real.instNeg im	—	Real.instIsOrderedAddMonoid Real.instArchimedean Nat.instAtLeastTwoHAddOfNat Real.two_pi_pos exp_mul_I ofReal_exp toIocMod.eq_1 ofReal_sub ofReal_zsmul ofReal_mul Function.Periodic.sub_zsmul_eq exp_mul_I_periodic exp_add re_add_im arg_mul_cos_add_sin_mul_I Real.exp_pos Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_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.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero 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.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add toIocMod_mem_Ioc
arg_exp_mul_I 📖	mathematical	—	arg exp Complex instMul ofReal I toIocMod Real Real.instAddCommGroup Real.linearOrder Real.instIsOrderedAddMonoid Real.instArchimedean Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Real.two_pi_pos Real.instNeg	—	Real.instIsOrderedAddMonoid Real.instArchimedean Nat.instAtLeastTwoHAddOfNat Real.two_pi_pos arg_exp toIocMod.congr_simp mul_one MulZeroClass.mul_zero add_zero
arg_inv 📖	mathematical	—	arg Complex instInv Real Real.pi Real.decidableEq Real.instNeg	—	arg_conj inv_def mul_comm map_zero MonoidWithZeroHomClass.toZeroHomClass MonoidWithZeroHom.monoidWithZeroHomClass inv_zero RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.mul_zero arg_zero arg_real_mul PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing
arg_inv_coe_angle 📖	mathematical	—	Real.Angle.coe arg Complex instInv Real.Angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	arg_inv Real.Angle.neg_coe_pi
arg_le_pi 📖	mathematical	—	Real Real.instLE arg Real.pi	—	arg_mem_Ioc
arg_le_pi_div_two_iff 📖	mathematical	—	Real Real.instLE arg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instZero re Real.instLT im	—	Nat.instAtLeastTwoHAddOfNat le_or_gt arg_of_re_nonneg LT.lt.not_ge LE.le.not_gt not_le arg_of_re_neg_of_im_nonneg sub_lt_iff_lt_add IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid half_sub CharZero.NeZero.two RCLike.charZero_rclike Real.neg_pi_div_two_lt_arcsin neg_im neg_div neg_lt_neg_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd div_lt_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing norm_pos_iff LT.lt.ne abs_of_nonneg abs_im_lt_norm arg_of_re_neg_of_im_neg LE.le.trans sub_le_self LT.lt.le Real.pi_pos Real.arcsin_le_pi_div_two
arg_lt_pi_div_two_iff 📖	mathematical	—	Real Real.instLT arg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instZero re im Complex instZero	—	Nat.instAtLeastTwoHAddOfNat lt_iff_le_and_ne arg_le_pi_div_two_iff arg_eq_pi_div_two_iff lt_trichotomy LT.lt.ne LT.lt.not_ge LT.lt.not_gt LT.lt.le LT.lt.ne'
arg_lt_pi_iff 📖	mathematical	—	Real Real.instLT arg Real.pi Real.instLE Real.instZero re	—	LE.le.lt_iff_ne arg_le_pi not_iff_comm not_le arg_eq_pi_iff
arg_mem_Ioc 📖	mathematical	—	Real Set Set.instMembership Set.Ioc Real.instPreorder Real.instNeg Real.pi arg	—	Real.pi_pos eq_or_ne arg_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.le Nat.instAtLeastTwoHAddOfNat existsUnique_add_zsmul_mem_Ioc Real.instArchimedean Real.two_pi_pos norm_mul_cos_add_sin_mul_I cos_add_int_mul_two_pi sin_add_int_mul_two_pi arg_mul_cos_add_sin_mul_I norm_pos_iff zsmul_eq_mul two_mul neg_add_cancel_left ofReal_add ofReal_mul
arg_mul 📖	mathematical	Real Set Set.instMembership Set.Ioc Real.instPreorder Real.instNeg Real.pi Real.instAdd arg	Complex instMul	—	arg_mul_eq_add_arg_iff
arg_mul_coe_angle 📖	mathematical	—	Real.Angle.coe arg Complex instMul Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	ofReal_cos ofReal_sin cos_add_sin_I ofReal_add add_mul Distrib.rightDistribClass exp_add ofReal_mul mul_assoc mul_comm norm_mul_exp_arg_mul_I arg_mul_cos_add_sin_mul_I_coe_angle mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing norm_pos_iff
arg_mul_cos_add_sin_mul_I 📖	mathematical	Real Real.instLT Real.instZero Set Set.instMembership Set.Ioc Real.instPreorder Real.instNeg Real.pi	arg Complex instMul ofReal instAdd cos sin I	—	norm_mul NormedDivisionRing.toNormMulClass norm_of_nonneg LT.lt.le norm_cos_add_sin_mul_I mul_one re_ofReal_mul mul_nonneg_iff_right_nonneg_of_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing im_ofReal_mul mul_div_cancel_left₀ GroupWithZero.toMulDivCancelClass LT.lt.ne' neg_div Nat.instAtLeastTwoHAddOfNat Real.cos_nonneg_of_mem_Icc Real.arcsin_sin' not_le not_and_or Set.mem_Icc neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.cos_add_pi Real.cos_pos_of_mem_Ioo lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_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.neg_congr Nat.cast_one Mathlib.Tactic.Ring.one_mul 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.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat 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 Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.add_neg CancelDenoms.sub_subst CancelDenoms.neg_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true CancelDenoms.add_subst Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.sin_neg_of_neg_of_neg_pi_lt LT.lt.not_ge Real.sin_add_pi Real.arcsin_sin le_of_not_gt add_sub_cancel_right Real.cos_neg_of_pi_div_two_lt_of_lt Real.sin_nonneg_of_mem_Icc Real.sin_sub_pi sub_add_cancel
arg_mul_cos_add_sin_mul_I_coe_angle 📖	mathematical	Real Real.instLT Real.instZero	Real.Angle.coe arg Complex instMul ofReal instAdd Real.Angle.cos Real.Angle.sin I	—	Real.Angle.induction_on Real.instIsOrderedAddMonoid Real.instArchimedean Nat.instAtLeastTwoHAddOfNat Real.two_pi_pos ofReal_cos ofReal_sin arg_mul_cos_add_sin_mul_I_eq_toIocMod Real.Angle.coe_toIocMod
arg_mul_cos_add_sin_mul_I_eq_toIocMod 📖	mathematical	Real Real.instLT Real.instZero	arg Complex instMul ofReal instAdd cos sin I toIocMod Real.instAddCommGroup Real.linearOrder Real.instIsOrderedAddMonoid Real.instArchimedean Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Real.two_pi_pos Real.instNeg	—	Real.instIsOrderedAddMonoid Real.instArchimedean Nat.instAtLeastTwoHAddOfNat Real.two_pi_pos arg_real_mul exp_mul_I arg_exp_mul_I
arg_mul_cos_add_sin_mul_I_sub 📖	mathematical	Real Real.instLT Real.instZero	Real.instSub arg Complex instMul ofReal instAdd cos sin I Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Real.instIntCast Int.floor Real.instRing Real.linearOrder Real.instFloorRing DivInvMonoid.toDiv Real.instDivInvMonoid	—	Nat.instAtLeastTwoHAddOfNat Real.instIsOrderedAddMonoid Real.instArchimedean Real.two_pi_pos arg_mul_cos_add_sin_mul_I_eq_toIocMod toIocMod_sub_self IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Real.instIsStrictOrderedRing FloorRing.archimedean toIocDiv_eq_neg_floor zsmul_eq_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_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.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.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul 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.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.nnrat_rawCast Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.RingNF.rat_rawCast_neg Mathlib.Tactic.RingNF.int_rawCast_neg add_zero mul_one
arg_mul_eq_add_arg_iff 📖	mathematical	—	arg Complex instMul Real Real.instAdd Set Set.instMembership Set.Ioc Real.instPreorder Real.instNeg Real.pi	—	arg_coe_angle_toReal_eq_arg arg_mul_coe_angle Real.Angle.coe_add Real.Angle.toReal_coe_eq_self_iff_mem_Ioc
arg_mul_real 📖	mathematical	Real Real.instLT Real.instZero	arg Complex instMul ofReal	—	arg_real_mul mul_comm
arg_neg_I 📖	mathematical	—	arg Complex instNeg I Real Real.instNeg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat neg_zero norm_neg norm_I div_one Real.arcsin_neg Real.arcsin_one
arg_neg_coe_angle 📖	mathematical	—	Real.Angle.coe arg Complex instNeg Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.pi	—	lt_trichotomy arg_neg_eq_arg_add_pi_of_im_neg Real.Angle.coe_add ext arg_ofReal_of_neg ofReal_neg arg_ofReal_of_nonneg LT.lt.le Left.neg_pos_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.instAtLeastTwoHAddOfNat two_mul Real.Angle.coe_two_pi Real.Angle.coe_zero Left.neg_neg_iff zero_add arg_neg_eq_arg_sub_pi_of_im_pos Real.Angle.coe_sub Real.Angle.sub_coe_pi_eq_add_coe_pi
arg_neg_eq_arg_add_pi_iff 📖	mathematical	—	arg Complex instNeg Real Real.instAdd Real.pi Real.instLT im Real.instZero re	—	lt_trichotomy arg_neg_eq_arg_add_pi_of_im_neg ext arg_ofReal_of_neg ofReal_neg arg_ofReal_of_nonneg LT.lt.le Left.neg_pos_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.instAtLeastTwoHAddOfNat NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass RCLike.charZero_rclike LT.lt.not_gt neg_zero arg_zero zero_add Real.pi_ne_zero Left.neg_neg_iff arg_neg_eq_arg_sub_pi_of_im_pos sub_eq_add_neg LT.lt.ne
arg_neg_eq_arg_add_pi_of_im_neg 📖	mathematical	Real Real.instLT im Real.instZero	arg Complex instNeg Real.instAdd Real.pi	—	arg_of_im_neg arg_of_im_pos Left.neg_pos_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid norm_neg neg_div Real.arccos_neg add_comm
arg_neg_eq_arg_sub_pi_iff 📖	mathematical	—	arg Complex instNeg Real Real.instSub Real.pi Real.instLT Real.instZero im re	—	lt_trichotomy arg_neg_eq_arg_add_pi_of_im_neg sub_eq_add_neg AddLeftCancelSemigroup.toIsLeftCancelAdd NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass RCLike.charZero_rclike LT.lt.not_gt LT.lt.ne ext arg_ofReal_of_neg ofReal_neg arg_ofReal_of_nonneg LT.lt.le Left.neg_pos_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid sub_self neg_zero arg_zero zero_sub Left.neg_neg_iff arg_neg_eq_arg_sub_pi_of_im_pos
arg_neg_eq_arg_sub_pi_of_im_pos 📖	mathematical	Real Real.instLT Real.instZero im	arg Complex instNeg Real.instSub Real.pi	—	arg_of_im_pos arg_of_im_neg Left.neg_neg_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid norm_neg neg_div Real.arccos_neg neg_sub
arg_neg_iff 📖	mathematical	—	Real Real.instLT arg Real.instZero im	—	lt_iff_lt_of_le_iff_le arg_nonneg_iff
arg_neg_one 📖	mathematical	—	arg Complex instNeg instOne Real.pi	—	IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid not_le zero_lt_one' Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike neg_zero neg_neg norm_neg CStarRing.norm_of_mem_unitary RCLike.instCStarRing instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass div_one Real.arcsin_zero zero_add
arg_nonneg_iff 📖	mathematical	—	Real Real.instLE Real.instZero arg im	—	eq_or_ne arg_zero Real.sin_nonneg_of_mem_Icc arg_le_pi Mathlib.Tactic.Contrapose.contrapose₁ Real.sin_neg_of_neg_of_neg_pi_lt neg_pi_lt_arg sin_arg le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing norm_pos_iff MulZeroClass.zero_mul
arg_ofReal_of_neg 📖	mathematical	Real Real.instLT Real.instZero	arg ofReal Real.pi	—	arg_eq_pi_iff
arg_ofReal_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero	arg ofReal	—	norm_real zero_div Real.arcsin_zero
arg_of_im_neg 📖	mathematical	Real Real.instLT im Real.instZero	arg Real.instNeg Real.arccos DivInvMonoid.toDiv Real.instDivInvMonoid re Norm.norm Complex instNorm	—	LT.lt.ne cos_arg Real.cos_neg Real.arccos_cos neg_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.le arg_neg_iff neg_le covariant_swap_add_of_covariant_add neg_pi_lt_arg neg_neg
arg_of_im_nonneg_of_ne_zero 📖	mathematical	Real Real.instLE Real.instZero im	arg Real.arccos DivInvMonoid.toDiv Real.instDivInvMonoid re Norm.norm Complex instNorm	—	cos_arg Real.arccos_cos arg_nonneg_iff arg_le_pi
arg_of_im_pos 📖	mathematical	Real Real.instLT Real.instZero im	arg Real.arccos DivInvMonoid.toDiv Real.instDivInvMonoid re Norm.norm Complex instNorm	—	arg_of_im_nonneg_of_ne_zero LT.lt.le LT.lt.ne'
arg_of_re_neg_of_im_neg 📖	mathematical	Real Real.instLT re Real.instZero im	arg Real.instSub Real.arcsin DivInvMonoid.toDiv Real.instDivInvMonoid Complex instNeg Norm.norm instNorm Real.pi	—	LT.lt.not_ge
arg_of_re_neg_of_im_nonneg 📖	mathematical	Real Real.instLT re Real.instZero Real.instLE im	arg Real.instAdd Real.arcsin DivInvMonoid.toDiv Real.instDivInvMonoid Complex instNeg Norm.norm instNorm Real.pi	—	LT.lt.not_ge
arg_of_re_nonneg 📖	mathematical	Real Real.instLE Real.instZero re	arg Real.arcsin DivInvMonoid.toDiv Real.instDivInvMonoid im Norm.norm Complex instNorm	—	—
arg_one 📖	mathematical	—	arg Complex instOne Real Real.instZero	—	Real.instZeroLEOneClass CStarRing.norm_of_mem_unitary RCLike.instCStarRing instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass div_one Real.arcsin_zero
arg_pow_coe_angle 📖	mathematical	—	Real.Angle.coe arg Complex Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring Real.Angle AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instNormedAddCommGroupAngle ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	eq_or_ne pow_zero arg_one arg_zero nsmul_zero zero_pow zero_nsmul pow_succ arg_mul_coe_angle pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass succ_nsmul
arg_real_mul 📖	mathematical	Real Real.instLT Real.instZero	arg Complex instMul ofReal	—	eq_or_ne MulZeroClass.mul_zero norm_mul_cos_add_sin_mul_I mul_assoc ofReal_mul arg_mul_cos_add_sin_mul_I mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing norm_pos_iff arg_mem_Ioc
arg_zero 📖	mathematical	—	arg Complex instZero Real Real.instZero	—	norm_zero div_zero Real.arcsin_zero
arg_zpow_coe_angle 📖	mathematical	—	Real.Angle.coe arg Complex DivInvMonoid.toZPow instDivInvMonoid Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle	—	zpow_natCast arg_pow_coe_angle natCast_zsmul zpow_negSucc arg_inv_coe_angle negSucc_zsmul
continuousAt_arg 📖	mathematical	Complex Set Set.instMembership slitPlane	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Real.pseudoMetricSpace arg	—	norm_ne_zero_iff slitPlane_ne_zero lt_or_lt_iff_ne mem_slitPlane_iff ContinuousAt.congr ContinuousAt.comp Real.continuousAt_arcsin ContinuousAt.div IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.continuousAt continuous_im continuous_norm Filter.EventuallyEq.symm arg_eq_nhds_of_re_pos ContinuousAt.neg IsTopologicalRing.toContinuousNeg Real.continuous_arccos continuous_re arg_eq_nhds_of_im_neg arg_eq_nhds_of_im_pos
continuousAt_arg_coe_angle 📖	mathematical	—	ContinuousAt Complex Real.Angle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instNormedAddCommGroupAngle Real Real.Angle.coe arg	—	ContinuousAt.comp Continuous.continuousAt Real.Angle.continuous_coe continuousAt_arg neg_neg Function.comp_assoc Function.update_eq_iff arg_zero zero_add arg_neg_coe_angle Function.mt mem_slitPlane_iff ContinuousAt.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup neg_re neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LE.le.lt_of_ne ext_iff continuousAt_const continuousAt_update_of_ne T2Space.t1Space instT2Space neg_ne_zero ContinuousNeg.continuous_neg IsTopologicalRing.toContinuousNeg IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing
continuousOn_arg 📖	mathematical	—	ContinuousOn Complex Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Real.pseudoMetricSpace arg slitPlane	—	ContinuousAt.continuousWithinAt continuousAt_arg
continuousWithinAt_arg_of_re_neg_of_im_zero 📖	mathematical	Real Real.instLT re Real.instZero im	ContinuousWithinAt Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Real.pseudoMetricSpace arg setOf Real.instLE	—	Continuous.tendsto continuous_re gt_mem_nhds instOrderTopologyReal Filter.mp_mem mem_nhdsWithin_of_mem_nhds self_mem_nhdsWithin Filter.univ_mem' arg.eq_1 LT.lt.not_ge ContinuousWithinAt.congr_of_eventuallyEq ContinuousWithinAt.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousAt.comp_continuousWithinAt Real.continuousAt_arcsin ContinuousWithinAt.div IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal IsTopologicalSemiring.toContinuousMul Continuous.continuousAt continuous_im continuousWithinAt_neg IsTopologicalRing.toContinuousNeg IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Continuous.continuousWithinAt continuous_norm CanLift.prf canLift norm_real IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add LT.lt.ne tendsto_const_nhds Eq.ge
cos_arg 📖	mathematical	—	Real.cos arg Real DivInvMonoid.toDiv Real.instDivInvMonoid re Norm.norm Complex instNorm	—	arg.eq_1 Real.cos_arcsin 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.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt norm_pos_iff 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.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.div_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 Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial sq_norm_sub_sq_im Real.sqrt_div IsOrderedRing.toPosMulMono Real.instIsOrderedRing Real.sqrt_sq LT.lt.le Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Real.cos_add_pi mul_neg Even.neg_pow Nat.instAtLeastTwoHAddOfNat sq_nonneg AddGroup.existsAddOfLE IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.sqrt_sq_eq_abs abs_of_neg not_le neg_div neg_neg Real.cos_sub_pi
exp_mem_slitPlane 📖	mathematical	—	Complex Set Set.instMembership slitPlane exp	—	Real.instIsOrderedAddMonoid Real.instArchimedean Nat.instAtLeastTwoHAddOfNat Real.two_pi_pos arg_exp
ext_norm_arg 📖	—	Norm.norm Complex instNorm arg	—	—	norm_mul_exp_arg_mul_I
ext_norm_arg_iff 📖	mathematical	—	Norm.norm Complex instNorm arg	—	ext_norm_arg
image_exp_Ioc_eq_sphere 📖	mathematical	—	Set.image Real Complex exp instMul ofReal I Set.Ioc Real.instPreorder Real.instNeg Real.pi Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instZero Real.instOne	—	Set.ext sub_zero norm_eq_one_iff'
mem_slitPlane_iff_arg 📖	mathematical	—	Complex Set Set.instMembership slitPlane	—	—
natCast_arg 📖	mathematical	—	arg Complex instNatCast Real Real.instZero	—	arg_ofReal_of_nonneg Nat.cast_nonneg Real.instIsOrderedRing ofReal_natCast
neg_pi_div_two_le_arg_iff 📖	mathematical	—	Real Real.instLE Real.instNeg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat arg Real.instZero re im	—	Nat.instAtLeastTwoHAddOfNat le_or_gt arg_of_re_nonneg LT.lt.not_ge arg_of_re_neg_of_im_nonneg LE.le.trans Real.neg_pi_div_two_le_arcsin le_add_of_nonneg_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.le Real.pi_pos not_le arg_of_re_neg_of_im_neg sub_lt_iff_lt_add' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd sub_eq_add_neg sub_half CharZero.NeZero.two RCLike.charZero_rclike Real.arcsin_lt_pi_div_two div_lt_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing norm_pos_iff LT.lt.ne neg_im abs_of_neg abs_im_lt_norm
neg_pi_div_two_lt_arg_iff 📖	mathematical	—	Real Real.instLT Real.instNeg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat arg Real.instZero re Real.instLE im	—	Nat.instAtLeastTwoHAddOfNat lt_iff_le_and_ne neg_pi_div_two_le_arg_iff arg_eq_neg_pi_div_two_iff lt_trichotomy LT.lt.not_ge LT.lt.ne LT.lt.not_gt LT.lt.le LT.lt.ne'
neg_pi_lt_arg 📖	mathematical	—	Real Real.instLT Real.instNeg Real.pi arg	—	arg_mem_Ioc
norm_eq_one_iff 📖	mathematical	—	Norm.norm Complex instNorm Real Real.instOne exp instMul ofReal I	—	ofReal_one one_mul norm_mul_exp_arg_mul_I norm_exp_ofReal_mul_I
norm_eq_one_iff' 📖	mathematical	—	Norm.norm Complex instNorm Real Real.instOne Set Set.instMembership Set.Ioc Real.instPreorder Real.instNeg Real.pi exp instMul ofReal I	—	norm_eq_one_iff Real.instIsOrderedAddMonoid Real.instArchimedean Nat.instAtLeastTwoHAddOfNat mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing two_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono Real.pi_pos Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_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.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero 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.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add toIocMod_mem_Ioc eq_sub_of_add_eq toIocMod_add_toIocDiv_zsmul ofReal_sub ofReal_zsmul ofReal_mul ofReal_ofNat Function.Periodic.sub_zsmul_eq exp_mul_I_periodic
norm_mul_cos_add_sin_mul_I 📖	mathematical	—	Complex instMul ofReal Norm.norm instNorm instAdd cos arg sin I	—	exp_mul_I norm_mul_exp_arg_mul_I
norm_mul_cos_arg 📖	mathematical	—	Real Real.instMul Norm.norm Complex instNorm Real.cos arg re	—	MulZeroClass.mul_zero sin_ofReal_im mul_one sub_self add_zero cos_ofReal_im zero_add MulZeroClass.zero_mul sub_zero norm_mul_cos_add_sin_mul_I
norm_mul_exp_arg_mul_I 📖	mathematical	—	Complex instMul ofReal Norm.norm instNorm exp arg I	—	eq_or_ne norm_zero MulZeroClass.zero_mul norm_ne_zero_iff ext exp_ofReal_mul_I_re cos_arg mul_comm IsUnit.div_mul_cancel exp_ofReal_mul_I_im sin_arg sub_zero add_zero
norm_mul_sin_arg 📖	mathematical	—	Real Real.instMul Norm.norm Complex instNorm Real.sin arg im	—	cos_ofReal_im mul_one sin_ofReal_im MulZeroClass.mul_zero add_zero zero_add sub_self MulZeroClass.zero_mul norm_mul_cos_add_sin_mul_I
ofNat_arg 📖	mathematical	—	arg Real Real.instZero	—	natCast_arg
range_arg 📖	mathematical	—	Set.range Real Complex arg Set.Ioc Real.instPreorder Real.instNeg Real.pi	—	HasSubset.Subset.antisymm Set.instAntisymmSubset Set.range_subset_iff arg_mem_Ioc arg_cos_add_sin_mul_I
range_exp_mul_I 📖	mathematical	—	Set.range Complex Real exp instMul ofReal I Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instZero Real.instOne	—	Set.ext
sin_arg 📖	mathematical	—	Real.sin arg Real DivInvMonoid.toDiv Real.instDivInvMonoid im Norm.norm Complex instNorm	—	Real.sin_arcsin abs_le Real.instIsOrderedAddMonoid abs_im_div_norm_le_one neg_div Real.arcsin_neg Real.sin_add Real.sin_neg Real.cos_pi mul_neg mul_one neg_neg Real.cos_neg Real.sin_pi MulZeroClass.mul_zero add_zero sub_eq_add_neg neg_zero
slitPlane_arg_ne_pi 📖	—	Complex Set Set.instMembership slitPlane	—	—	mem_slitPlane_iff_arg
tan_arg 📖	mathematical	—	Real.tan arg Real DivInvMonoid.toDiv Real.instDivInvMonoid im re	—	arg_zero Real.tan_zero zero_div Real.tan_eq_sin_div_cos sin_arg cos_arg div_div_div_cancel_right₀ norm_ne_zero_iff
tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero 📖	mathematical	Real Real.instLT re Real.instZero im	Filter.Tendsto Complex arg nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf nhds Real.pseudoMetricSpace Real.instNeg Real.pi	—	neg_zero zero_div Real.arcsin_zero zero_sub Filter.Tendsto.sub_const IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal ContinuousAt.comp_continuousWithinAt Real.continuousAt_arcsin ContinuousWithinAt.div IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.continuousAt continuous_im continuousWithinAt_neg IsTopologicalRing.toContinuousNeg IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Continuous.continuousWithinAt continuous_norm CanLift.prf canLift norm_real IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add LT.lt.ne Filter.Tendsto.congr' Continuous.tendsto continuous_re gt_mem_nhds instOrderTopologyReal Filter.mp_mem mem_nhdsWithin_of_mem_nhds self_mem_nhdsWithin Filter.univ_mem' arg.eq_1 LT.lt.not_ge
tendsto_arg_nhdsWithin_im_nonneg_of_re_neg_of_im_zero 📖	mathematical	Real Real.instLT re Real.instZero im	Filter.Tendsto Complex arg nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf Real.instLE nhds Real.pseudoMetricSpace Real.pi	—	arg_eq_pi_iff ContinuousWithinAt.tendsto continuousWithinAt_arg_of_re_neg_of_im_zero
toIocMod_arg 📖	mathematical	—	toIocMod Real Real.instAddCommGroup Real.linearOrder Real.instIsOrderedAddMonoid Real.instArchimedean Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Real.two_pi_pos Real.instNeg arg	—	Real.instIsOrderedAddMonoid Real.instArchimedean Nat.instAtLeastTwoHAddOfNat Real.two_pi_pos two_mul toIocMod.congr_simp neg_add_cancel_left arg_mem_Ioc

Mathlib.Meta.FunProp.Mor

Definitions

Name	Category	Theorems
Arg 📖	CompData	—

---

← Back to Index