Arg

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

Statistics

Metric	Count
Definitions	0
Theorems norm_add_eq, norm_add_eq_iff, norm_sub_eq, norm_sub_eq_iff, sameRay_iff, sameRay_iff_arg_div_eq_zero, sameRay_of_arg_eq	7
Total	7

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_add_eq 📖	mathematical	arg	Norm.norm Complex instNorm instAdd Real Real.instAdd	—	SameRay.norm_add sameRay_of_arg_eq
norm_add_eq_iff 📖	mathematical	—	Norm.norm Complex instNorm instAdd Real Real.instAdd instZero arg	—	Real.instIsStrictOrderedRing sameRay_iff_norm_add UniformConvexSpace.toStrictConvexSpace InnerProductSpace.toUniformConvexSpace sameRay_iff
norm_sub_eq 📖	mathematical	arg	Norm.norm Complex instNorm instSub Real Real.norm Real.instSub	—	SameRay.norm_sub sameRay_of_arg_eq
norm_sub_eq_iff 📖	mathematical	—	Norm.norm Complex instNorm instSub abs Real Real.lattice Real.instAddGroup Real.instSub instZero arg	—	Real.instIsStrictOrderedRing sameRay_iff_norm_sub UniformConvexSpace.toStrictConvexSpace InnerProductSpace.toUniformConvexSpace sameRay_iff
sameRay_iff 📖	mathematical	—	SameRay Real Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex instZero arg	—	Real.instIsStrictOrderedRing eq_or_ne arg_zero arg_eq_arg_iff Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero 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.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.NF.cons_ne_zero mul_comm
sameRay_iff_arg_div_eq_zero 📖	mathematical	—	SameRay Real Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex arg DivInvMonoid.toDiv instDivInvMonoid Real.instZero	—	Real.instIsStrictOrderedRing Real.Angle.toReal_zero arg_coe_angle_eq_iff_eq_toReal sameRay_iff arg_zero zero_div div_zero arg_div_coe_angle
sameRay_of_arg_eq 📖	mathematical	arg	SameRay Real Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex	—	Real.instIsStrictOrderedRing sameRay_iff

---

← Back to Index