Angle

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

Statistics

Metric	Count
Definitions	0
Theorems angle_div_left_eq_angle_mul_right, angle_div_right_eq_angle_mul_left, angle_eq_abs_arg, angle_exp_exp, angle_exp_one, angle_le_mul_norm_sub, angle_mul_left, angle_mul_right, angle_one_left, angle_one_right, mul_angle_le_norm_sub, norm_sub_le_angle, norm_sub_mem_Icc_angle	13
Total	13

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
angle_div_left_eq_angle_mul_right 📖	mathematical	—	InnerProductGeometry.angle Complex instNormedAddCommGroup instInnerProductSpaceRealComplex DivInvMonoid.toDiv instDivInvMonoid instMul	—	eq_or_ne Nat.instAtLeastTwoHAddOfNat div_zero InnerProductGeometry.angle_zero_left MulZeroClass.mul_zero InnerProductGeometry.angle_zero_right angle_mul_right div_mul_cancel₀
angle_div_right_eq_angle_mul_left 📖	mathematical	—	InnerProductGeometry.angle Complex instNormedAddCommGroup instInnerProductSpaceRealComplex DivInvMonoid.toDiv instDivInvMonoid instMul	—	InnerProductGeometry.angle_comm angle_div_left_eq_angle_mul_right
angle_eq_abs_arg 📖	mathematical	—	InnerProductGeometry.angle Complex instNormedAddCommGroup instInnerProductSpaceRealComplex abs Real Real.lattice Real.instAddGroup arg DivInvMonoid.toDiv instDivInvMonoid	—	Real.arccos_eq_of_eq_cos abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add abs_arg_le_pi Real.cos_abs cos_arg div_ne_zero mul_neg sub_neg_eq_add div_eq_mul_inv mul_inv_rev inv_re normSq_eq_norm_sq inv_im neg_mul norm_mul norm_inv inv_inv 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.subst_add 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 Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero ne_of_gt norm_pos_iff one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
angle_exp_exp 📖	mathematical	—	InnerProductGeometry.angle Complex instNormedAddCommGroup instInnerProductSpaceRealComplex exp instMul ofReal I abs Real Real.lattice Real.instAddGroup 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.instSub	—	Real.instIsOrderedAddMonoid Real.instArchimedean Nat.instAtLeastTwoHAddOfNat Real.two_pi_pos angle_eq_abs_arg exp_ne_zero arg_exp_mul_I
angle_exp_one 📖	mathematical	—	InnerProductGeometry.angle Complex instNormedAddCommGroup instInnerProductSpaceRealComplex exp instMul ofReal I instOne abs Real Real.lattice Real.instAddGroup 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 MulZeroClass.zero_mul exp_zero toIocMod.congr_simp sub_zero angle_exp_exp
angle_le_mul_norm_sub 📖	mathematical	Norm.norm Complex instNorm Real Real.instOne	Real.instLE InnerProductGeometry.angle instNormedAddCommGroup instInnerProductSpaceRealComplex Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat instSub	—	Nat.instAtLeastTwoHAddOfNat div_le_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing div_pos Real.pi_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo div_eq_inv_mul inv_div mul_angle_le_norm_sub
angle_mul_left 📖	mathematical	—	InnerProductGeometry.angle Complex instNormedAddCommGroup instInnerProductSpaceRealComplex instMul	—	eq_or_ne Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero InnerProductGeometry.angle_zero_right InnerProductGeometry.angle_zero_left angle_eq_abs_arg NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass mul_div_mul_left
angle_mul_right 📖	mathematical	—	InnerProductGeometry.angle Complex instNormedAddCommGroup instInnerProductSpaceRealComplex instMul	—	mul_comm angle_mul_left
angle_one_left 📖	mathematical	—	InnerProductGeometry.angle Complex instNormedAddCommGroup instInnerProductSpaceRealComplex instOne abs Real Real.lattice Real.instAddGroup arg	—	angle_eq_abs_arg NeZero.charZero_one instCharZero one_div abs_arg_inv
angle_one_right 📖	mathematical	—	InnerProductGeometry.angle Complex instNormedAddCommGroup instInnerProductSpaceRealComplex instOne abs Real Real.lattice Real.instAddGroup arg	—	angle_eq_abs_arg NeZero.charZero_one instCharZero div_one
mul_angle_le_norm_sub 📖	mathematical	Norm.norm Complex instNorm Real Real.instOne	Real.instLE Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi InnerProductGeometry.angle instNormedAddCommGroup instInnerProductSpaceRealComplex instSub	—	Nat.instAtLeastTwoHAddOfNat norm_sub_mem_Icc_angle
norm_sub_le_angle 📖	mathematical	Norm.norm Complex instNorm Real Real.instOne	Real.instLE instSub InnerProductGeometry.angle instNormedAddCommGroup instInnerProductSpaceRealComplex	—	Nat.instAtLeastTwoHAddOfNat norm_sub_mem_Icc_angle
norm_sub_mem_Icc_angle 📖	mathematical	Norm.norm Complex instNorm Real Real.instOne	Set Set.instMembership Set.Icc Real.instPreorder Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi InnerProductGeometry.angle instNormedAddCommGroup instInnerProductSpaceRealComplex instSub	—	Nat.instAtLeastTwoHAddOfNat norm_eq_one_iff' Real.instIsOrderedAddMonoid Real.instArchimedean Real.two_pi_pos angle_exp_one exp_mul_I add_sub_right_comm toIocMod_eq_self Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_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.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 Nat.cast_one norm_add_mul_I Real.le_sqrt_of_sq_le mul_pow abs_pow Real.instIsOrderedRing abs_sq Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isNat_mul mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono sub_le_sub_left IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add Real.cos_le_one_sub_mul_cos_sq abs_le Set.Ioc_subset_Icc_self le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Real.cos_sq_add_sin_sq Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Real.sqrt_le_left abs_nonneg Real.one_sub_sq_div_two_le_cos Mathlib.Meta.NormNum.IsNNRat.to_raw_eq 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.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Meta.NormNum.isNNRat_mul norm_div div_one NormOneClass.norm_one NormedDivisionRing.to_normOneClass one_mul div_sub_one norm_zero NeZero.charZero_one angle_div_left_eq_angle_mul_right

---

← Back to Index