Basic

📁 Source: Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean

Statistics

Metric	Count
Definitions oangle	1
Theorems oangle, abs_oangle_sub_left_toReal_lt_pi_div_two, abs_oangle_sub_right_toReal_lt_pi_div_two, angle_eq_abs_oangle_toReal, angle_eq_iff_oangle_eq_neg_of_sign_eq_neg, angle_eq_iff_oangle_eq_of_sign_eq, angle_eq_iff_oangle_eq_or_sameRay, continuousAt_oangle, cos_oangle_eq_cos_angle, cos_oangle_eq_inner_div_norm_mul_norm, eq_iff_norm_eq_and_oangle_eq_zero, eq_iff_norm_eq_of_oangle_eq_zero, eq_iff_oangle_eq_zero_of_norm_eq, eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero, eq_zero_or_oangle_eq_iff_inner_eq_zero, inner_eq_norm_mul_norm_mul_cos_oangle, inner_eq_zero_of_oangle_eq_neg_pi_div_two, inner_eq_zero_of_oangle_eq_pi_div_two, inner_rev_eq_zero_of_oangle_eq_neg_pi_div_two, inner_rev_eq_zero_of_oangle_eq_pi_div_two, left_ne_zero_of_oangle_eq_neg_pi_div_two, left_ne_zero_of_oangle_eq_pi, left_ne_zero_of_oangle_eq_pi_div_two, left_ne_zero_of_oangle_ne_zero, left_ne_zero_of_oangle_sign_eq_neg_one, left_ne_zero_of_oangle_sign_eq_one, left_ne_zero_of_oangle_sign_ne_zero, ne_of_oangle_eq_neg_pi_div_two, ne_of_oangle_eq_pi, ne_of_oangle_eq_pi_div_two, ne_of_oangle_ne_zero, ne_of_oangle_sign_eq_neg_one, ne_of_oangle_sign_eq_one, ne_of_oangle_sign_ne_zero, oangle_add, oangle_add_cyc3, oangle_add_cyc3_neg_left, oangle_add_cyc3_neg_right, oangle_add_oangle_rev, oangle_add_oangle_rev_neg_left, oangle_add_oangle_rev_neg_right, oangle_add_swap, oangle_eq_angle_of_sign_eq_one, oangle_eq_angle_or_eq_neg_angle, oangle_eq_neg_angle_of_sign_eq_neg_one, oangle_eq_neg_of_angle_eq_of_sign_eq_neg, oangle_eq_of_angle_eq_of_sign_eq, oangle_eq_pi_iff_angle_eq_pi, oangle_eq_pi_iff_oangle_rev_eq_pi, oangle_eq_pi_iff_sameRay_neg, oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq, oangle_eq_zero_iff_angle_eq_zero, oangle_eq_zero_iff_oangle_rev_eq_zero, oangle_eq_zero_iff_sameRay, oangle_eq_zero_or_eq_pi_iff_not_linearIndependent, oangle_eq_zero_or_eq_pi_iff_right_eq_smul, oangle_map, oangle_map_complex, oangle_ne_zero_and_ne_pi_iff_linearIndependent, oangle_neg_left, oangle_neg_left_eq_neg_right, oangle_neg_neg, oangle_neg_orientation_eq_neg, oangle_neg_right, oangle_neg_self_left, oangle_neg_self_right, oangle_rev, oangle_self, oangle_sign_add_left, oangle_sign_add_right, oangle_sign_add_smul_left, oangle_sign_neg_left, oangle_sign_neg_right, oangle_sign_smul_add_right, oangle_sign_smul_add_smul_left, oangle_sign_smul_add_smul_right, oangle_sign_smul_add_smul_smul_add_smul, oangle_sign_smul_left, oangle_sign_smul_right, oangle_sign_smul_sub_left, oangle_sign_smul_sub_right, oangle_sign_sub_left, oangle_sign_sub_left_eq_neg, oangle_sign_sub_left_swap, oangle_sign_sub_right, oangle_sign_sub_right_eq_neg, oangle_sign_sub_right_swap, oangle_sign_sub_smul_left, oangle_sign_sub_smul_right, oangle_smul_add_right_eq_zero_or_eq_pi_iff, oangle_smul_left_of_neg, oangle_smul_left_of_pos, oangle_smul_left_self_of_nonneg, oangle_smul_right_of_neg, oangle_smul_right_of_pos, oangle_smul_right_self_of_nonneg, oangle_smul_smul_self_of_nonneg, oangle_sub_eq_oangle_sub_rev_of_norm_eq, oangle_sub_left, oangle_sub_right, oangle_zero_left, oangle_zero_right, right_ne_zero_of_oangle_eq_neg_pi_div_two, right_ne_zero_of_oangle_eq_pi, right_ne_zero_of_oangle_eq_pi_div_two, right_ne_zero_of_oangle_ne_zero, right_ne_zero_of_oangle_sign_eq_neg_one, right_ne_zero_of_oangle_sign_eq_one, right_ne_zero_of_oangle_sign_ne_zero, two_zsmul_oangle_left_of_span_eq, two_zsmul_oangle_neg_left, two_zsmul_oangle_neg_right, two_zsmul_oangle_neg_self_left, two_zsmul_oangle_neg_self_right, two_zsmul_oangle_of_span_eq_of_span_eq, two_zsmul_oangle_right_of_span_eq, two_zsmul_oangle_smul_left_of_ne_zero, two_zsmul_oangle_smul_left_self, two_zsmul_oangle_smul_right_of_ne_zero, two_zsmul_oangle_smul_right_self, two_zsmul_oangle_smul_smul_self	121
Total	122

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
oangle 📖	mathematical	—	Orientation.oangle Complex instNormedAddCommGroup instInnerProductSpaceRealComplex finrank_real_complex_fact orientation Real.Angle.coe arg instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	finrank_real_complex_fact smulCommClass_self kahler mul_comm

Orientation

Definitions

Name	Category	Theorems
oangle 📖	CompOp	108 math math: oangle_sign_smul_add_right, oangle_eq_zero_or_eq_pi_iff_right_eq_smul, oangle_add, oangle_add_swap, oangle_sign_sub_left_swap, oangle_add_left_smul_rotation_pi_div_two, oangle_eq_zero_iff_oangle_rev_eq_zero, eq_iff_norm_eq_and_oangle_eq_zero, tan_oangle_add_left_smul_rotation_pi_div_two, oangle_eq_two_zsmul_oangle_sub_of_norm_eq, two_zsmul_oangle_smul_left_of_ne_zero, two_zsmul_oangle_neg_left, oangle_zero_left, tan_oangle_add_right_smul_rotation_pi_div_two, Complex.oangle, two_zsmul_oangle_neg_self_right, oangle_eq_pi_iff_oangle_rev_eq_pi, oangle_neg_right, oangle_sign_sub_right, oangle_smul_left_of_neg, oangle_sign_sub_smul_left, oangle_eq_pi_iff_angle_eq_pi, oangle_neg_left_eq_neg_right, oangle_sign_sub_smul_right, oangle_smul_left_self_of_nonneg, oangle_eq_angle_or_eq_neg_angle, oangle_neg_self_left, oangle_eq_zero_iff_sameRay, angle_eq_iff_oangle_eq_or_sameRay, oangle_rotation_left, oangle_eq_zero_iff_angle_eq_zero, oangle_rotation_oangle_right, oangle_add_oangle_rev, oangle_self, oangle_rotation, oangle_rotation_self_left, oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero, inner_eq_norm_mul_norm_mul_cos_oangle, oangle_sign_neg_left, oangle_sub_eq_oangle_sub_rev_of_norm_eq, two_zsmul_oangle_of_span_eq_of_span_eq, oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero, oangle_neg_left, oangle_rotation_oangle_left, oangle_sign_smul_left, oangle_sign_sub_right_eq_neg, oangle_sign_smul_add_smul_smul_add_smul, oangle_sign_smul_sub_left, oangle_zero_right, oangle_rotation_right, oangle_sub_left, continuousAt_oangle, oangle_sub_right_smul_rotation_pi_div_two, oangle_sign_sub_left_eq_neg, oangle_add_cyc3, oangle_neg_self_right, oangle_sign_sub_left, cos_oangle_eq_cos_angle, oangle_eq_zero_or_eq_pi_iff_not_linearIndependent, oangle_sign_smul_right, oangle_sign_add_smul_left, oangle_sub_left_smul_rotation_pi_div_two, oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero, oangle_add_right_smul_rotation_pi_div_two, oangle_sign_sub_right_swap, oangle_smul_right_of_neg, two_zsmul_oangle_neg_self_left, oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq, oangle_add_cyc3_neg_left, oangle_map, oangle_smul_smul_self_of_nonneg, eq_zero_or_oangle_eq_iff_inner_eq_zero, oangle_sign_add_left, two_zsmul_oangle_smul_right_self, oangle_sign_neg_right, angle_eq_abs_oangle_toReal, oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero, oangle_rev, oangle_add_oangle_rev_neg_left, two_zsmul_oangle_neg_right, two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq, two_zsmul_oangle_smul_right_of_ne_zero, eq_iff_oangle_eq_zero_of_norm_eq, oangle_smul_add_right_eq_zero_or_eq_pi_iff, two_zsmul_oangle_left_of_span_eq, two_zsmul_oangle_smul_left_self, abs_oangle_sub_left_toReal_lt_pi_div_two, oangle_sign_smul_add_smul_right, oangle_eq_pi_iff_sameRay_neg, oangle_rotation_self_right, oangle_sign_add_right, oangle_smul_right_of_pos, oangle_map_complex, oangle_neg_neg, oangle_smul_right_self_of_nonneg, oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real, oangle_neg_orientation_eq_neg, oangle_sign_smul_add_smul_left, oangle_sub_right, two_zsmul_oangle_smul_smul_self, rotation_oangle_eq_iff_norm_eq, oangle_sign_smul_sub_right, oangle_add_cyc3_neg_right, cos_oangle_eq_inner_div_norm_mul_norm, two_zsmul_oangle_right_of_span_eq, abs_oangle_sub_right_toReal_lt_pi_div_two, oangle_smul_left_of_pos, oangle_add_oangle_rev_neg_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_oangle_sub_left_toReal_lt_pi_div_two 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm	Real Real.instLT abs Real.lattice Real.instAddGroup Real.Angle.toReal oangle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat oangle.congr_simp sub_self oangle_zero_left Real.Angle.toReal_zero abs_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsOrderedRing Real.instNontrivial oangle_sign_sub_left_swap oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq Real.Angle.sign_pi_sub Real.Angle.sign_two_zsmul_eq_sign_iff neg_sub oangle_eq_pi_iff_sameRay_neg oangle_eq_pi_iff_oangle_rev_eq_pi exists_nonneg_left_iff_sameRay one_smul zero_add add_eq_right AddRightCancelSemigroup.toIsRightCancelAdd norm_ne_zero_iff mul_left_eq_self₀ IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain abs_of_pos Left.add_pos_of_nonneg_of_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd one_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Real.norm_eq_abs norm_smul NormedSpace.toNormSMulClass add_smul eq_sub_iff_add_eq
abs_oangle_sub_right_toReal_lt_pi_div_two 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm	Real Real.instLT abs Real.lattice Real.instAddGroup Real.Angle.toReal oangle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat abs_oangle_sub_left_toReal_lt_pi_div_two oangle_sub_eq_oangle_sub_rev_of_norm_eq
angle_eq_abs_oangle_toReal 📖	mathematical	—	InnerProductGeometry.angle abs Real Real.lattice Real.instAddGroup Real.Angle.toReal oangle	—	Real.instIsStrictOrderedRing InnerProductGeometry.angle_nonneg InnerProductGeometry.angle_le_pi oangle_eq_angle_or_eq_neg_angle Real.Angle.abs_toReal_coe_eq_self_iff Real.Angle.abs_toReal_neg_coe_eq_self_iff
angle_eq_iff_oangle_eq_neg_of_sign_eq_neg 📖	mathematical	Real.Angle.sign oangle SignType SignType.instNeg	InnerProductGeometry.angle Real.Angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing oangle_rev InnerProductGeometry.angle_comm angle_eq_iff_oangle_eq_of_sign_eq Real.Angle.sign_neg
angle_eq_iff_oangle_eq_of_sign_eq 📖	mathematical	Real.Angle.sign oangle	InnerProductGeometry.angle	—	Real.instIsStrictOrderedRing oangle_eq_of_angle_eq_of_sign_eq angle_eq_abs_oangle_toReal
angle_eq_iff_oangle_eq_or_sameRay 📖	mathematical	—	InnerProductGeometry.angle oangle SameRay Real Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat InnerProductGeometry.angle_zero_right InnerProductGeometry.angle_zero_left oangle.congr_simp oangle_zero_right oangle_zero_left SameRay.exists_pos_left InnerProductGeometry.angle_smul_right_of_pos InnerProductGeometry.angle_comm oangle_smul_right_of_pos angle_eq_iff_oangle_eq_of_sign_eq oangle_eq_zero_iff_sameRay oangle_add angle_eq_iff_oangle_eq_neg_of_sign_eq_neg neg_add_cancel eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero InnerProductGeometry.angle_eq_zero_iff oangle_self Real.Angle.sign_zero InnerProductGeometry.angle_eq_pi_iff oangle_smul_right_of_neg oangle_neg_self_right Real.Angle.sign_coe_pi instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Real.instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero
continuousAt_oangle 📖	mathematical	—	ContinuousAt Real.Angle instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instNormedAddCommGroupAngle oangle	—	Real.instIsStrictOrderedRing ContinuousAt.comp Complex.continuousAt_arg_coe_angle kahler_ne_zero Continuous.continuousAt SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Continuous.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Continuous.comp Complex.continuous_ofReal continuous_inner Continuous.mul IsTopologicalSemiring.toContinuousMul ContinuousLinearMap.continuous₂ continuous_const
cos_oangle_eq_cos_angle 📖	mathematical	—	Real.Angle.cos oangle Real.cos InnerProductGeometry.angle	—	Real.instIsStrictOrderedRing cos_oangle_eq_inner_div_norm_mul_norm InnerProductGeometry.cos_angle
cos_oangle_eq_inner_div_norm_mul_norm 📖	mathematical	—	Real.Angle.cos oangle Real DivInvMonoid.toDiv Real.instDivInvMonoid Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instMul Norm.norm NormedAddCommGroup.toNorm	—	Real.instIsStrictOrderedRing inner_eq_norm_mul_norm_mul_cos_oangle Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul 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.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt norm_pos_iff one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf
eq_iff_norm_eq_and_oangle_eq_zero 📖	mathematical	—	Norm.norm NormedAddCommGroup.toNorm oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing oangle_eq_zero_iff_sameRay SameRay.refl eq_or_ne norm_zero SameRay.exists_nonneg_right one_smul mul_right_cancel₀ IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain one_mul norm_smul NormedSpace.toNormSMulClass abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
eq_iff_norm_eq_of_oangle_eq_zero 📖	mathematical	oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	Norm.norm NormedAddCommGroup.toNorm	—	Real.instIsStrictOrderedRing eq_iff_norm_eq_and_oangle_eq_zero
eq_iff_oangle_eq_zero_of_norm_eq 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm	oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing eq_iff_norm_eq_and_oangle_eq_zero
eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero 📖	mathematical	Real.Angle.sign oangle SignType SignType.instZero	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup InnerProductGeometry.angle Real Real.instZero Real.pi	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat InnerProductGeometry.angle_zero_left RCLike.charZero_rclike InnerProductGeometry.angle_zero_right angle_eq_abs_oangle_toReal Real.Angle.sign_eq_zero_iff Real.Angle.toReal_zero abs_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.Angle.toReal_pi covariant_swap_add_of_covariant_add LT.lt.le Real.pi_pos
eq_zero_or_oangle_eq_iff_inner_eq_zero 📖	mathematical	—	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup oangle Real.Angle.coe Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instNeg Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instZero	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat oangle.congr_simp oangle_zero_left inner_zero_left oangle_zero_right inner_zero_right InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two angle_eq_abs_oangle_toReal Real.Angle.abs_toReal_eq_pi_div_two_iff neg_div oangle_eq_angle_or_eq_neg_angle
inner_eq_norm_mul_norm_mul_cos_oangle 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instMul Norm.norm NormedAddCommGroup.toNorm Real.Angle.cos oangle	—	Real.instIsStrictOrderedRing inner_zero_left norm_zero MulZeroClass.zero_mul oangle.congr_simp oangle_zero_left Real.Angle.cos_zero mul_one inner_zero_right MulZeroClass.mul_zero oangle_zero_right oangle.eq_1 Real.Angle.cos_coe Complex.cos_arg kahler_ne_zero smulCommClass_self norm_kahler Algebra.to_smulCommClass sub_self add_zero Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul 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.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_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 ne_of_gt norm_pos_iff one_ne_zero NeZero.one GroupWithZero.toNontrivial
inner_eq_zero_of_oangle_eq_neg_pi_div_two 📖	mathematical	oangle Real.Angle.coe Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNeg Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instZero	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat eq_zero_or_oangle_eq_iff_inner_eq_zero
inner_eq_zero_of_oangle_eq_pi_div_two 📖	mathematical	oangle Real.Angle.coe Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instZero	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat eq_zero_or_oangle_eq_iff_inner_eq_zero
inner_rev_eq_zero_of_oangle_eq_neg_pi_div_two 📖	mathematical	oangle Real.Angle.coe Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNeg Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instZero	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat real_inner_comm inner_eq_zero_of_oangle_eq_neg_pi_div_two
inner_rev_eq_zero_of_oangle_eq_pi_div_two 📖	mathematical	oangle Real.Angle.coe Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instZero	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat real_inner_comm inner_eq_zero_of_oangle_eq_pi_div_two
left_ne_zero_of_oangle_eq_neg_pi_div_two 📖	—	oangle Real.Angle.coe Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNeg Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat left_ne_zero_of_oangle_ne_zero Real.Angle.neg_pi_div_two_ne_zero
left_ne_zero_of_oangle_eq_pi 📖	—	oangle Real.Angle.coe Real.pi	—	—	Real.instIsStrictOrderedRing left_ne_zero_of_oangle_ne_zero Real.Angle.pi_ne_zero
left_ne_zero_of_oangle_eq_pi_div_two 📖	—	oangle Real.Angle.coe Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat left_ne_zero_of_oangle_ne_zero Real.Angle.pi_div_two_ne_zero
left_ne_zero_of_oangle_ne_zero 📖	—	—	—	—	Real.instIsStrictOrderedRing oangle_zero_left
left_ne_zero_of_oangle_sign_eq_neg_one 📖	—	Real.Angle.sign oangle SignType SignType.instNeg SignType.instOne	—	—	Real.instIsStrictOrderedRing left_ne_zero_of_oangle_sign_ne_zero
left_ne_zero_of_oangle_sign_eq_one 📖	—	Real.Angle.sign oangle SignType SignType.instOne	—	—	Real.instIsStrictOrderedRing left_ne_zero_of_oangle_sign_ne_zero
left_ne_zero_of_oangle_sign_ne_zero 📖	—	—	—	—	Real.instIsStrictOrderedRing left_ne_zero_of_oangle_ne_zero Real.Angle.sign_ne_zero_iff
ne_of_oangle_eq_neg_pi_div_two 📖	—	oangle Real.Angle.coe Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNeg Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat ne_of_oangle_ne_zero Real.Angle.neg_pi_div_two_ne_zero
ne_of_oangle_eq_pi 📖	—	oangle Real.Angle.coe Real.pi	—	—	Real.instIsStrictOrderedRing ne_of_oangle_ne_zero Real.Angle.pi_ne_zero
ne_of_oangle_eq_pi_div_two 📖	—	oangle Real.Angle.coe Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat ne_of_oangle_ne_zero Real.Angle.pi_div_two_ne_zero
ne_of_oangle_ne_zero 📖	—	—	—	—	Real.instIsStrictOrderedRing oangle_self
ne_of_oangle_sign_eq_neg_one 📖	—	Real.Angle.sign oangle SignType SignType.instNeg SignType.instOne	—	—	Real.instIsStrictOrderedRing ne_of_oangle_sign_ne_zero
ne_of_oangle_sign_eq_one 📖	—	Real.Angle.sign oangle SignType SignType.instOne	—	—	Real.instIsStrictOrderedRing ne_of_oangle_sign_ne_zero
ne_of_oangle_sign_ne_zero 📖	—	—	—	—	Real.instIsStrictOrderedRing ne_of_oangle_ne_zero Real.Angle.sign_ne_zero_iff
oangle_add 📖	mathematical	—	Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid oangle	—	Real.instIsStrictOrderedRing Complex.arg_mul_coe_angle kahler_ne_zero smulCommClass_self kahler_mul Complex.arg_real_mul pow_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass norm_pos_iff
oangle_add_cyc3 📖	mathematical	—	Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid oangle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing oangle_add oangle_add_oangle_rev
oangle_add_cyc3_neg_left 📖	mathematical	—	Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid oangle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.Angle.coe Real.pi	—	Real.instIsStrictOrderedRing oangle_neg_left Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat oangle_add_cyc3 Real.Angle.coe_pi_add_coe_pi
oangle_add_cyc3_neg_right 📖	mathematical	—	Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid oangle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.Angle.coe Real.pi	—	Real.instIsStrictOrderedRing oangle_add_cyc3_neg_left
oangle_add_oangle_rev 📖	mathematical	—	Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid oangle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing oangle_rev neg_add_cancel
oangle_add_oangle_rev_neg_left 📖	mathematical	—	Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid oangle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NegZeroClass.toZero	—	Real.instIsStrictOrderedRing oangle_neg_left_eq_neg_right oangle_rev neg_add_cancel
oangle_add_oangle_rev_neg_right 📖	mathematical	—	Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid oangle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NegZeroClass.toZero	—	Real.instIsStrictOrderedRing oangle_rev oangle_neg_left_eq_neg_right add_neg_cancel
oangle_add_swap 📖	mathematical	—	Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid oangle	—	Real.instIsStrictOrderedRing add_comm oangle_add
oangle_eq_angle_of_sign_eq_one 📖	mathematical	Real.Angle.sign oangle SignType SignType.instOne	Real.Angle.coe InnerProductGeometry.angle	—	Real.instIsStrictOrderedRing oangle.congr_simp oangle_zero_left Real.Angle.sign_zero NeZero.one GroupWithZero.toNontrivial oangle_zero_right oangle_eq_angle_or_eq_neg_angle not_le SignType.neg_iff neg_eq_iff_eq_neg Real.Angle.sign_neg Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi InnerProductGeometry.angle_nonneg InnerProductGeometry.angle_le_pi
oangle_eq_angle_or_eq_neg_angle 📖	mathematical	—	oangle Real.Angle.coe InnerProductGeometry.angle Real.Angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing Real.Angle.cos_eq_real_cos_iff_eq_or_eq_neg cos_oangle_eq_cos_angle
oangle_eq_neg_angle_of_sign_eq_neg_one 📖	mathematical	Real.Angle.sign oangle SignType SignType.instNeg SignType.instOne	Real.Angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle Real.Angle.coe InnerProductGeometry.angle	—	Real.instIsStrictOrderedRing oangle.congr_simp oangle_zero_left Real.Angle.sign_zero oangle_zero_right oangle_eq_angle_or_eq_neg_angle not_le SignType.neg_iff Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi InnerProductGeometry.angle_nonneg InnerProductGeometry.angle_le_pi
oangle_eq_neg_of_angle_eq_of_sign_eq_neg 📖	mathematical	InnerProductGeometry.angle Real.Angle.sign oangle SignType SignType.instNeg	Real.Angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing oangle_rev oangle_eq_of_angle_eq_of_sign_eq InnerProductGeometry.angle_comm Real.Angle.sign_neg
oangle_eq_of_angle_eq_of_sign_eq 📖	—	InnerProductGeometry.angle Real.Angle.sign oangle	—	—	Real.instIsStrictOrderedRing oangle_zero_left Real.Angle.sign_zero oangle_zero_right Nat.instAtLeastTwoHAddOfNat InnerProductGeometry.angle_zero_left InnerProductGeometry.angle_zero_right LT.lt.ne Real.pi_pos add_sub_cancel_right mul_two sub_eq_zero div_eq_iff two_ne_zero CharZero.NeZero.two RCLike.charZero_rclike eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero oangle.congr_simp Real.Angle.eq_iff_abs_toReal_eq_of_sign_eq angle_eq_abs_oangle_toReal
oangle_eq_pi_iff_angle_eq_pi 📖	mathematical	—	oangle Real.Angle.coe Real.pi InnerProductGeometry.angle	—	Real.instIsStrictOrderedRing oangle.congr_simp oangle_zero_left Real.Angle.pi_ne_zero Nat.instAtLeastTwoHAddOfNat InnerProductGeometry.angle_zero_left div_eq_mul_inv IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain RCLike.charZero_rclike oangle_zero_right InnerProductGeometry.angle_zero_right angle_eq_abs_oangle_toReal Real.Angle.toReal_pi Real.instIsOrderedAddMonoid LT.lt.le Real.pi_pos oangle_eq_angle_or_eq_neg_angle Real.Angle.neg_coe_pi
oangle_eq_pi_iff_oangle_rev_eq_pi 📖	mathematical	—	oangle Real.Angle.coe Real.pi	—	Real.instIsStrictOrderedRing oangle_rev neg_eq_iff_eq_neg Real.Angle.neg_coe_pi
oangle_eq_pi_iff_sameRay_neg 📖	mathematical	—	oangle Real.Angle.coe Real.pi SameRay Real Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing oangle_eq_zero_iff_sameRay oangle.congr_simp oangle_zero_left Real.Angle.pi_ne_zero oangle_zero_right oangle_neg_right Real.Angle.coe_pi_add_coe_pi sub_eq_zero Real.Angle.sub_coe_pi_eq_add_coe_pi
oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm	oangle Real.Angle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle Real.Angle.coe Real.pi SubNegMonoid.toZSMul	—	Real.instIsStrictOrderedRing two_zsmul oangle_sub_eq_oangle_sub_rev_of_norm_eq eq_sub_iff_add_eq oangle_neg_neg add_assoc norm_eq_zero norm_zero norm_ne_zero_iff oangle.congr_simp neg_sub neg_neg oangle_add_cyc3_neg_right neg_ne_zero sub_ne_zero_of_ne
oangle_eq_zero_iff_angle_eq_zero 📖	mathematical	—	oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle InnerProductGeometry.angle Real Real.instZero	—	Real.instIsStrictOrderedRing angle_eq_abs_oangle_toReal IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add oangle_eq_angle_or_eq_neg_angle neg_zero
oangle_eq_zero_iff_oangle_rev_eq_zero 📖	mathematical	—	oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing oangle_rev neg_eq_zero
oangle_eq_zero_iff_sameRay 📖	mathematical	—	oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle SameRay Real Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	Real.instIsStrictOrderedRing oangle.eq_1 Algebra.to_smulCommClass smulCommClass_self kahler_apply_apply Complex.arg_coe_angle_eq_iff_eq_toReal Real.Angle.toReal_zero Complex.arg_eq_zero_iff MulZeroClass.mul_zero mul_one sub_self add_zero zero_add nonneg_inner_and_areaForm_eq_zero_iff_sameRay
oangle_eq_zero_or_eq_pi_iff_not_linearIndependent 📖	mathematical	—	oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle Real.Angle.coe Real.pi LinearIndependent Real Matrix.vecCons Matrix.vecEmpty Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	Real.instIsStrictOrderedRing oangle_eq_zero_iff_sameRay oangle_eq_pi_iff_sameRay_neg sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Real.instIsDomain GroupWithZero.toNoZeroSMulDivisors
oangle_eq_zero_or_eq_pi_iff_right_eq_smul 📖	mathematical	—	oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle Real.Angle.coe Real.pi Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	Real.instIsStrictOrderedRing oangle_eq_zero_iff_sameRay oangle_eq_pi_iff_sameRay_neg smul_zero SameRay.exists_nonneg_left neg_smul neg_neg SameRay.congr_simp neg_zero lt_trichotomy smul_ne_zero instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Real.instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero LT.lt.ne SameRay.sameRay_pos_smul_right PosSMulMono.toSMulPosMono Real.instIsOrderedRing Real.instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule IsScalarTower.left Left.neg_pos_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono zero_smul
oangle_map 📖	mathematical	—	oangle DFunLike.coe Equiv Orientation Real Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike Equiv.instEquivLike map LinearIsometryEquiv.toLinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearIsometryEquiv LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm	—	Real.instIsStrictOrderedRing RingHomInvPair.ids smulCommClass_self kahler_map
oangle_map_complex 📖	mathematical	DFunLike.coe Equiv Orientation Real Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Complex NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instInnerProductSpaceRealComplex EquivLike.toFunLike Equiv.instEquivLike map LinearIsometryEquiv.toLinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex.orientation	oangle Real.Angle.coe Complex.arg Complex.instMul RingHom CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing LinearIsometryEquiv LinearIsometryEquiv.instEquivLike	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Complex.finrank_real_complex_fact Complex.oangle oangle_map LinearIsometryEquiv.symm_apply_apply
oangle_ne_zero_and_ne_pi_iff_linearIndependent 📖	mathematical	—	LinearIndependent Real Matrix.vecCons Matrix.vecEmpty Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	Real.instIsStrictOrderedRing Mathlib.Tactic.Contrapose.contrapose_iff₁ Mathlib.Tactic.Push.not_and_or_eq oangle_eq_zero_or_eq_pi_iff_not_linearIndependent
oangle_neg_left 📖	mathematical	—	oangle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup 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.Angle.coe Real.pi	—	Real.instIsStrictOrderedRing map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Complex.arg_neg_coe_angle kahler_ne_zero
oangle_neg_left_eq_neg_right 📖	mathematical	—	oangle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing neg_neg oangle_neg_neg
oangle_neg_neg 📖	mathematical	—	oangle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass neg_neg
oangle_neg_orientation_eq_neg 📖	mathematical	—	oangle Orientation Real Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike instNegRay Real.commRing AlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommGroup Real.instAddCommGroup AlternatingMap.instModule Real.Angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing smulCommClass_self kahler_neg_orientation Complex.arg_conj_coe_angle
oangle_neg_right 📖	mathematical	—	oangle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup 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.Angle.coe Real.pi	—	Real.instIsStrictOrderedRing map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Complex.arg_neg_coe_angle kahler_ne_zero
oangle_neg_self_left 📖	mathematical	—	oangle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.Angle.coe Real.pi	—	Real.instIsStrictOrderedRing oangle_neg_left oangle_self zero_add
oangle_neg_self_right 📖	mathematical	—	oangle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.Angle.coe Real.pi	—	Real.instIsStrictOrderedRing oangle_neg_right oangle_self zero_add
oangle_rev 📖	mathematical	—	oangle Real.Angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing smulCommClass_self kahler_swap Complex.arg_conj_coe_angle
oangle_self 📖	mathematical	—	oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing oangle.eq_1 smulCommClass_self kahler_apply_self Complex.ofReal_pow Nat.instAtLeastTwoHAddOfNat AddSubgroup.normal_of_comm Complex.arg_ofReal_of_nonneg Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE even_two_mul QuotientAddGroup.mk_zero
oangle_sign_add_left 📖	mathematical	—	Real.Angle.sign oangle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Real.instIsStrictOrderedRing oangle_sign_add_smul_left one_smul
oangle_sign_add_right 📖	mathematical	—	Real.Angle.sign oangle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Real.instIsStrictOrderedRing oangle_sign_smul_add_right one_smul
oangle_sign_add_smul_left 📖	mathematical	—	Real.Angle.sign oangle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	Real.instIsStrictOrderedRing oangle_rev Real.Angle.sign_neg oangle.congr_simp add_comm oangle_sign_smul_add_right
oangle_sign_neg_left 📖	mathematical	—	Real.Angle.sign oangle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SignType SignType.instNeg	—	Real.instIsStrictOrderedRing oangle.congr_simp neg_zero oangle_zero_left Real.Angle.sign_zero oangle_zero_right oangle_neg_left Real.Angle.sign_add_pi
oangle_sign_neg_right 📖	mathematical	—	Real.Angle.sign oangle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SignType SignType.instNeg	—	Real.instIsStrictOrderedRing oangle.congr_simp oangle_zero_left Real.Angle.sign_zero neg_zero oangle_zero_right oangle_neg_right Real.Angle.sign_add_pi
oangle_sign_smul_add_right 📖	mathematical	—	Real.Angle.sign oangle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	Real.instIsStrictOrderedRing Real.Angle.sign_eq_zero_iff oangle_smul_add_right_eq_zero_or_eq_pi_iff IsConnected.image isConnected_univ PathConnectedSpace.connectedSpace Real.instPathConnectedSpace ContinuousOn.prodMk continuousOn_const ContinuousOn.fun_add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousOn.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul continuousOn_id' continuousOn_of_forall_continuousAt continuousAt_oangle oangle.congr_simp smul_zero zero_add oangle_zero_left oangle_zero_right zero_smul Set.mem_image_of_mem Set.mem_univ Real.Angle.sign_eq_of_continuousOn
oangle_sign_smul_add_smul_left 📖	mathematical	—	Real.Angle.sign oangle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike SignType SignType.instMul DFunLike.coe OrderHom Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT	—	Real.instIsStrictOrderedRing oangle_rev Real.Angle.sign_neg oangle.congr_simp add_comm oangle_sign_smul_add_smul_right mul_neg
oangle_sign_smul_add_smul_right 📖	mathematical	—	Real.Angle.sign oangle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike SignType SignType.instMul DFunLike.coe OrderHom Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT	—	Real.instIsStrictOrderedRing oangle_sign_smul_add_right oangle_sign_smul_right
oangle_sign_smul_add_smul_smul_add_smul 📖	mathematical	—	Real.Angle.sign oangle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike SignType SignType.instMul DFunLike.coe OrderHom Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT Real.instSub Real.instMul	—	Real.instIsStrictOrderedRing zero_smul MulZeroClass.zero_mul zero_add zero_sub Left.sign_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid oangle_sign_smul_left add_comm oangle_sign_smul_add_smul_right oangle_rev Real.Angle.sign_neg sign_mul mul_neg neg_mul mul_assoc oangle_sign_smul_add_right smul_add smul_smul div_mul_cancel₀ neg_smul add_assoc sub_eq_add_neg sub_add_cancel add_smul oangle_sign_smul_right oangle_sign_smul_add_smul_left add_mul Distrib.rightDistribClass mul_comm
oangle_sign_smul_left 📖	mathematical	—	Real.Angle.sign oangle Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike SignType SignType.instMul DFunLike.coe OrderHom Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT	—	Real.instIsStrictOrderedRing lt_trichotomy oangle_smul_left_of_neg oangle_sign_neg_left sign_neg neg_mul one_mul oangle.congr_simp zero_smul oangle_zero_left Real.Angle.sign_zero sign_zero MulZeroClass.zero_mul oangle_smul_left_of_pos sign_pos
oangle_sign_smul_right 📖	mathematical	—	Real.Angle.sign oangle Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike SignType SignType.instMul DFunLike.coe OrderHom Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT	—	Real.instIsStrictOrderedRing lt_trichotomy oangle_smul_right_of_neg oangle_sign_neg_right sign_neg neg_mul one_mul oangle.congr_simp zero_smul oangle_zero_right Real.Angle.sign_zero sign_zero MulZeroClass.zero_mul oangle_smul_right_of_pos sign_pos
oangle_sign_smul_sub_left 📖	mathematical	—	Real.Angle.sign oangle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike SignType SignType.instNeg	—	Real.instIsStrictOrderedRing oangle_sign_neg_left sub_eq_neg_add oangle_sign_add_smul_left
oangle_sign_smul_sub_right 📖	mathematical	—	Real.Angle.sign oangle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike SignType SignType.instNeg	—	Real.instIsStrictOrderedRing oangle_sign_neg_right sub_eq_add_neg oangle_sign_smul_add_right
oangle_sign_sub_left 📖	mathematical	—	Real.Angle.sign oangle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	Real.instIsStrictOrderedRing oangle_sign_sub_smul_left one_smul
oangle_sign_sub_left_eq_neg 📖	mathematical	—	Real.Angle.sign oangle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SignType SignType.instNeg	—	Real.instIsStrictOrderedRing oangle_sign_smul_sub_left one_smul
oangle_sign_sub_left_swap 📖	mathematical	—	Real.Angle.sign oangle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	Real.instIsStrictOrderedRing oangle_sign_sub_left_eq_neg oangle_rev Real.Angle.sign_neg
oangle_sign_sub_right 📖	mathematical	—	Real.Angle.sign oangle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	Real.instIsStrictOrderedRing oangle_sign_sub_smul_right one_smul
oangle_sign_sub_right_eq_neg 📖	mathematical	—	Real.Angle.sign oangle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SignType SignType.instNeg	—	Real.instIsStrictOrderedRing oangle_sign_smul_sub_right one_smul
oangle_sign_sub_right_swap 📖	mathematical	—	Real.Angle.sign oangle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	Real.instIsStrictOrderedRing oangle_sign_sub_right_eq_neg oangle_rev Real.Angle.sign_neg
oangle_sign_sub_smul_left 📖	mathematical	—	Real.Angle.sign oangle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	Real.instIsStrictOrderedRing sub_eq_add_neg neg_smul oangle_sign_add_smul_left
oangle_sign_sub_smul_right 📖	mathematical	—	Real.Angle.sign oangle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	Real.instIsStrictOrderedRing sub_eq_add_neg neg_smul add_comm oangle_sign_smul_add_right
oangle_smul_add_right_eq_zero_or_eq_pi_iff 📖	mathematical	—	oangle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle Real.Angle.coe Real.pi	—	Real.instIsStrictOrderedRing Fin.sum_univ_two add_smul add_assoc smul_smul smul_add not_and_or add_zero MulZeroClass.zero_mul sub_smul sub_add_cancel sub_zero
oangle_smul_left_of_neg 📖	mathematical	Real Real.instLT Real.instZero	oangle SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing neg_neg neg_smul smul_neg oangle_smul_left_of_pos neg_pos_of_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
oangle_smul_left_of_pos 📖	mathematical	Real Real.instLT Real.instZero	oangle SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	Real.instIsStrictOrderedRing smulCommClass_self map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass Complex.arg_real_mul
oangle_smul_left_self_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero	oangle SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing LE.le.lt_or_eq oangle_smul_left_of_pos oangle_self oangle.congr_simp zero_smul oangle_zero_left
oangle_smul_right_of_neg 📖	mathematical	Real Real.instLT Real.instZero	oangle SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing neg_neg neg_smul smul_neg oangle_smul_right_of_pos neg_pos_of_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
oangle_smul_right_of_pos 📖	mathematical	Real Real.instLT Real.instZero	oangle SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	Real.instIsStrictOrderedRing map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass Complex.arg_real_mul
oangle_smul_right_self_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero	oangle SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing LE.le.lt_or_eq oangle_smul_right_of_pos oangle_self oangle.congr_simp zero_smul oangle_zero_right
oangle_smul_smul_self_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero	oangle SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing LE.le.lt_or_eq oangle_smul_left_of_pos oangle_smul_right_self_of_nonneg oangle.congr_simp zero_smul oangle_zero_left
oangle_sub_eq_oangle_sub_rev_of_norm_eq 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm	oangle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	Real.instIsStrictOrderedRing map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass smulCommClass_self kahler_apply_self
oangle_sub_left 📖	mathematical	—	Real.Angle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle	—	Real.instIsStrictOrderedRing sub_eq_iff_eq_add oangle_add_swap
oangle_sub_right 📖	mathematical	—	Real.Angle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle	—	Real.instIsStrictOrderedRing sub_eq_iff_eq_add oangle_add
oangle_zero_left 📖	mathematical	—	oangle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.Angle Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Complex.arg_zero
oangle_zero_right 📖	mathematical	—	oangle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.Angle Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Complex.arg_zero
right_ne_zero_of_oangle_eq_neg_pi_div_two 📖	—	oangle Real.Angle.coe Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNeg Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat right_ne_zero_of_oangle_ne_zero Real.Angle.neg_pi_div_two_ne_zero
right_ne_zero_of_oangle_eq_pi 📖	—	oangle Real.Angle.coe Real.pi	—	—	Real.instIsStrictOrderedRing right_ne_zero_of_oangle_ne_zero Real.Angle.pi_ne_zero
right_ne_zero_of_oangle_eq_pi_div_two 📖	—	oangle Real.Angle.coe Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat right_ne_zero_of_oangle_ne_zero Real.Angle.pi_div_two_ne_zero
right_ne_zero_of_oangle_ne_zero 📖	—	—	—	—	Real.instIsStrictOrderedRing oangle_zero_right
right_ne_zero_of_oangle_sign_eq_neg_one 📖	—	Real.Angle.sign oangle SignType SignType.instNeg SignType.instOne	—	—	Real.instIsStrictOrderedRing right_ne_zero_of_oangle_sign_ne_zero
right_ne_zero_of_oangle_sign_eq_one 📖	—	Real.Angle.sign oangle SignType SignType.instOne	—	—	Real.instIsStrictOrderedRing right_ne_zero_of_oangle_sign_ne_zero
right_ne_zero_of_oangle_sign_ne_zero 📖	—	—	—	—	Real.instIsStrictOrderedRing right_ne_zero_of_oangle_ne_zero Real.Angle.sign_ne_zero_iff
two_zsmul_oangle_left_of_span_eq 📖	mathematical	Submodule.span Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Set Set.instSingletonSet	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle	—	Real.instIsStrictOrderedRing Submodule.span_singleton_eq_span_singleton Real.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors two_zsmul_oangle_smul_left_of_ne_zero Units.ne_zero Real.instNontrivial
two_zsmul_oangle_neg_left 📖	mathematical	—	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing oangle.congr_simp neg_zero oangle_zero_left smul_zero oangle_zero_right oangle_neg_left smul_add Real.Angle.two_zsmul_coe_pi add_zero
two_zsmul_oangle_neg_right 📖	mathematical	—	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing oangle.congr_simp oangle_zero_left smul_zero neg_zero oangle_zero_right oangle_neg_right smul_add Real.Angle.two_zsmul_coe_pi add_zero
two_zsmul_oangle_neg_self_left 📖	mathematical	—	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NegZeroClass.toZero	—	Real.instIsStrictOrderedRing oangle.congr_simp neg_zero oangle_self smul_zero oangle_neg_self_left Real.Angle.two_zsmul_coe_pi
two_zsmul_oangle_neg_self_right 📖	mathematical	—	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NegZeroClass.toZero	—	Real.instIsStrictOrderedRing oangle.congr_simp neg_zero oangle_self smul_zero oangle_neg_self_right Real.Angle.two_zsmul_coe_pi
two_zsmul_oangle_of_span_eq_of_span_eq 📖	mathematical	Submodule.span Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Set Set.instSingletonSet	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle	—	Real.instIsStrictOrderedRing two_zsmul_oangle_left_of_span_eq two_zsmul_oangle_right_of_span_eq
two_zsmul_oangle_right_of_span_eq 📖	mathematical	Submodule.span Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Set Set.instSingletonSet	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle	—	Real.instIsStrictOrderedRing Submodule.span_singleton_eq_span_singleton Real.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors two_zsmul_oangle_smul_right_of_ne_zero Units.ne_zero Real.instNontrivial
two_zsmul_oangle_smul_left_of_ne_zero 📖	mathematical	—	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	Real.instIsStrictOrderedRing Ne.lt_or_gt oangle_smul_left_of_neg two_zsmul_oangle_neg_left oangle_smul_left_of_pos
two_zsmul_oangle_smul_left_self 📖	mathematical	—	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing lt_or_ge oangle_smul_left_of_neg two_zsmul_oangle_neg_left oangle_self smul_zero oangle_smul_left_self_of_nonneg
two_zsmul_oangle_smul_right_of_ne_zero 📖	mathematical	—	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	Real.instIsStrictOrderedRing Ne.lt_or_gt oangle_smul_right_of_neg two_zsmul_oangle_neg_right oangle_smul_right_of_pos
two_zsmul_oangle_smul_right_self 📖	mathematical	—	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing lt_or_ge oangle_smul_right_of_neg two_zsmul_oangle_neg_right oangle_self smul_zero oangle_smul_right_self_of_nonneg
two_zsmul_oangle_smul_smul_self 📖	mathematical	—	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing oangle.congr_simp zero_smul oangle_zero_left smul_zero two_zsmul_oangle_smul_left_of_ne_zero two_zsmul_oangle_smul_right_self

---

← Back to Index