Affine

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

Statistics

Metric	Count
Definitions o, oangle, «term∡»	3
Theorems oangle_sign_eq_neg, oangle_sign_eq, oangle_sign_of_sameRay_vsub, two_zsmul_oangle_eq_left, two_zsmul_oangle_eq_right, abs_oangle_left_toReal_lt_pi_div_two_of_dist_eq, abs_oangle_right_toReal_lt_pi_div_two_of_dist_eq, affineIndependent_iff_of_two_zsmul_oangle_eq, 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_wbtw, angle_eq_pi_div_two_of_oangle_eq_neg_pi_div_two, angle_eq_pi_div_two_of_oangle_eq_pi_div_two, angle_rev_eq_pi_div_two_of_oangle_eq_neg_pi_div_two, angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two, collinear_iff_of_two_zsmul_oangle_eq, continuousAt_oangle, cos_oangle_eq_cos_angle, dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint, eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero, left_ne_of_oangle_eq_neg_pi_div_two, left_ne_of_oangle_eq_pi, left_ne_of_oangle_eq_pi_div_two, left_ne_of_oangle_ne_zero, left_ne_of_oangle_sign_eq_neg_one, left_ne_of_oangle_sign_eq_one, left_ne_of_oangle_sign_ne_zero, left_ne_right_of_oangle_eq_neg_pi_div_two, left_ne_right_of_oangle_eq_pi, left_ne_right_of_oangle_eq_pi_div_two, left_ne_right_of_oangle_ne_zero, left_ne_right_of_oangle_sign_eq_neg_one, left_ne_right_of_oangle_sign_eq_one, left_ne_right_of_oangle_sign_ne_zero, oangle_add, oangle_add_cyc3, oangle_add_oangle_rev, 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_oangle_of_dist_eq, oangle_eq_of_angle_eq_of_sign_eq, oangle_eq_of_parallel, oangle_eq_or_eq_neg_of_angle_eq, oangle_eq_pi_iff_angle_eq_pi, oangle_eq_pi_iff_oangle_rev_eq_pi, oangle_eq_pi_iff_sbtw, oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq, oangle_eq_zero_iff_angle_eq_zero, oangle_eq_zero_iff_oangle_rev_eq_zero, oangle_eq_zero_iff_wbtw, oangle_eq_zero_or_eq_pi_iff_collinear, oangle_homothety, oangle_midpoint_left, oangle_midpoint_rev_left, oangle_midpoint_rev_right, oangle_midpoint_right, oangle_ne_zero_and_ne_pi_iff_affineIndependent, oangle_ne_zero_and_ne_pi_iff_not_collinear, oangle_rev, oangle_rotate_sign, oangle_self_left, oangle_self_left_right, oangle_self_right, oangle_sign_eq_zero_iff_collinear, oangle_sub_left, oangle_sub_right, oangle_swap₁₂_sign, oangle_swap₁₃_sign, oangle_swap₂₃_sign, right_ne_of_oangle_eq_neg_pi_div_two, right_ne_of_oangle_eq_pi, right_ne_of_oangle_eq_pi_div_two, right_ne_of_oangle_ne_zero, right_ne_of_oangle_sign_eq_neg_one, right_ne_of_oangle_sign_eq_one, right_ne_of_oangle_sign_ne_zero, two_zsmul_oangle_of_parallel, two_zsmul_oangle_of_vectorSpan_eq, oangle_eq_add_pi_left, oangle_eq_add_pi_right, oangle_eq_left, oangle_eq_left_right, oangle_eq_right, oangle_sign_eq, oangle_sign_eq_left, oangle_sign_eq_of_sbtw, oangle_sign_eq_of_sbtw_left, oangle_sign_eq_right, oangle₁₂₃_eq_pi, oangle₁₃₂_eq_zero, oangle₂₁₃_eq_zero, oangle₂₃₁_eq_zero, oangle₃₁₂_eq_zero, oangle₃₂₁_eq_pi, oangle_eq_left, oangle_eq_right, oangle_sign_eq_of_ne_left, oangle_sign_eq_of_ne_right, oangle₁₃₂_eq_zero, oangle₂₁₃_eq_zero, oangle₂₃₁_eq_zero, oangle₃₁₂_eq_zero	106
Total	109

AffineSubspace.SOppSide

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
oangle_sign_eq_neg 📖	mathematical	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike AffineSubspace.SOppSide Real.commRing Real.partialOrder Real.instIsStrictOrderedRing	Real.Angle.sign EuclideanGeometry.oangle SignType SignType.instNeg	—	Real.instIsStrictOrderedRing left_notMem AffineSubspace.SSameSide.oangle_sign_eq trans symm AffineSubspace.sOppSide_pointReflection EuclideanGeometry.oangle_rotate_sign EuclideanGeometry.oangle_swap₁₃_sign Sbtw.oangle_sign_eq Sbtw.symm Real.instIsOrderedRing sbtw_pointReflection_of_ne

AffineSubspace.SSameSide

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
oangle_sign_eq 📖	mathematical	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike AffineSubspace.SSameSide Real.commRing Real.partialOrder Real.instIsStrictOrderedRing	Real.Angle.sign EuclideanGeometry.oangle	—	Real.instIsStrictOrderedRing EuclideanGeometry.oangle.congr_simp EuclideanGeometry.oangle_self_left_right Real.Angle.sign_zero IsConnected.image AffineSubspace.isConnected_setOf_sSameSide nonempty ContinuousOn.prodMk continuousOn_const continuousOn_id' continuousOn_of_forall_continuousAt EuclideanGeometry.continuousAt_oangle EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependent affineIndependent_of_ne_of_mem_of_notMem_of_mem Set.mem_image_of_mem AffineSubspace.sSameSide_self_iff Real.Angle.sign_eq_of_continuousOn

Collinear

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
oangle_sign_of_sameRay_vsub 📖	mathematical	Collinear Real Real.instDivisionRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instInsert Set.instSingletonSet SameRay Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	Real.Angle.sign EuclideanGeometry.oangle	—	Real.instIsStrictOrderedRing collinear_insert_iff_of_ne Set.mem_insert Set.mem_insert_of_mem Set.mem_singleton EuclideanGeometry.oangle_eq_zero_or_eq_pi_iff_collinear Set.insert_comm Real.Angle.sign_eq_zero_iff IsConnected.image IsConnected.prod isConnected_univ AddTorsor.connectedSpace instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyElemInsert ConnectedSpace.toPreconnectedSpace PathConnectedSpace.connectedSpace NormedSpace.instPathConnectedSpace IsScalarTower.left IsTopologicalAddTorsor.toContinuousVAdd AffineSubspace.instIsTopologicalAddTorsorSubtypeMemSubmoduleDirection instIsTopologicalAddTorsor_1 isConnected_setOf_sameRay_and_ne_zero vsub_ne_zero ContinuousOn.prodMk Continuous.comp_continuousOn' continuous_subtype_val ContinuousOn.fst continuousOn_id' continuousOn_const ContinuousOn.vadd ContinuousOn.snd continuousOn_of_forall_continuousAt EuclideanGeometry.continuousAt_oangle collinear_insert_iff_of_mem_affineSpan collinear_pair AffineSubspace.vadd_mem_of_mem_direction exists_nonneg_left_iff_sameRay direction_affineSpan smul_vsub_rev_mem_vectorSpan_pair EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependent affineIndependent_of_ne_of_mem_of_notMem_of_mem vsub_vadd_eq_vsub_sub vsub_self zero_sub neg_ne_zero left_mem_affineSpan_pair SameRay.rfl vsub_vadd mem_affineSpan_of_mem_of_ne Real.Angle.sign_eq_of_continuousOn
two_zsmul_oangle_eq_left 📖	mathematical	Collinear Real Real.instDivisionRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instInsert Set.instSingletonSet	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle EuclideanGeometry.oangle	—	Real.instIsStrictOrderedRing EuclideanGeometry.oangle.congr_simp EuclideanGeometry.oangle_self_right smul_zero wbtw_or_wbtw_or_wbtw Sbtw.oangle_eq_add_pi_left smul_add Real.Angle.two_zsmul_coe_pi add_zero Wbtw.oangle_eq_left Wbtw.symm Real.instIsOrderedRing
two_zsmul_oangle_eq_right 📖	mathematical	Collinear Real Real.instDivisionRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instInsert Set.instSingletonSet	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle EuclideanGeometry.oangle	—	Real.instIsStrictOrderedRing EuclideanGeometry.oangle_rev smul_neg two_zsmul_oangle_eq_left

EuclideanGeometry

Definitions

Name	Category	Theorems
o 📖	CompOp	5 math math: dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint, Sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, Affine.Triangle.circumsphere_eq_of_dist_of_oangle, Sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, Affine.Triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter
oangle 📖	CompOp	97 math math: oangle_swap₁₃_sign, Sbtw.oangle₁₂₃_eq_pi, abs_oangle_right_toReal_lt_pi_div_two_of_dist_eq, two_zsmul_oangle_of_parallel, oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq, Wbtw.oangle_eq_left, Sbtw.oangle_eq_add_pi_left, Wbtw.oangle_sign_eq_of_ne_left, oangle_eq_angle_or_eq_neg_angle, dist_orthogonalProjection_eq_iff_oangle_eq, oangle_sign_eq_zero_iff_collinear, oangle_self_left_right, oangle_rotate_sign, angle_eq_iff_oangle_eq_or_wbtw, oangle_midpoint_right, Wbtw.oangle₃₁₂_eq_zero, oangle_rev, Sphere.dist_div_sin_oangle_div_two_eq_radius, oangle_eq_zero_iff_angle_eq_zero, Wbtw.oangle₂₁₃_eq_zero, Sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_left, oangle_add, oangle_eq_zero_iff_oangle_rev_eq_zero, oangle_eq_pi_iff_sbtw, oangle_add_swap, Sbtw.oangle_sign_eq_right, oangle_midpoint_rev_left, Sbtw.oangle₂₃₁_eq_zero, Sbtw.oangle_eq_add_pi_right, Sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, oangle_eq_zero_iff_wbtw, Sbtw.oangle_sign_eq_of_sbtw, Sphere.dist_div_sin_oangle_eq_two_mul_radius, oangle_add_cyc3, Sbtw.oangle₃₂₁_eq_pi, oangle_sub_left, oangle_eq_pi_iff_angle_eq_pi, cos_oangle_eq_cos_angle, Affine.Triangle.circumsphere_eq_of_dist_of_oangle, two_zsmul_oangle_self_orthogonalProjection, oangle_midpoint_left, Sphere.abs_oangle_center_left_toReal_lt_pi_div_two, oangle_swap₁₂_sign, Sbtw.oangle_sign_eq, oangle_orthogonalProjection_self, Affine.Triangle.dist_div_sin_oangle_eq_two_mul_circumradius, Collinear.two_zsmul_oangle_eq_right, Sphere.dist_div_cos_oangle_center_div_two_eq_radius, oangle_add_oangle_add_oangle_eq_pi, Sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, oangle_eq_zero_or_eq_pi_iff_collinear, Sphere.abs_oangle_center_right_toReal_lt_pi_div_two, oangle_eq_of_dist_orthogonalProjection_eq, Affine.Triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter, Collinear.oangle_sign_of_sameRay_vsub, oangle_homothety, AffineSubspace.SSameSide.oangle_sign_eq, continuousAt_oangle, oangle_self_right, Sphere.dist_div_cos_oangle_center_eq_two_mul_radius, Wbtw.oangle_sign_eq_of_ne_right, Sbtw.oangle_eq_right, oangle_swap₂₃_sign, Wbtw.oangle₂₃₁_eq_zero, Sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_right, Sbtw.oangle₃₁₂_eq_zero, abs_oangle_left_toReal_lt_pi_div_two_of_dist_eq, oangle_eq_of_parallel, oangle_eq_or_eq_neg_of_angle_eq, oangle_midpoint_rev_right, Sbtw.oangle₁₃₂_eq_zero, Sbtw.oangle₂₁₃_eq_zero, angle_eq_abs_oangle_toReal, oangle_add_oangle_rev, abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two, Sphere.two_zsmul_oangle_eq, Sphere.two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi, oangle_self_orthogonalProjection, Sphere.oangle_center_eq_two_zsmul_oangle, Sbtw.oangle_eq_left_right, AffineSubspace.SOppSide.oangle_sign_eq_neg, oangle_eq_oangle_of_dist_eq, Sbtw.oangle_sign_eq_left, Collinear.two_zsmul_oangle_eq_left, Cospherical.two_zsmul_oangle_eq, Wbtw.oangle_eq_right, oangle_self_left, oangle_eq_pi_iff_oangle_rev_eq_pi, two_zsmul_oangle_eq_of_dist_orthogonalProjection_line_eq, two_zsmul_oangle_orthogonalProjection_self, Affine.Triangle.dist_div_sin_oangle_div_two_eq_circumradius, two_zsmul_oangle_of_vectorSpan_eq, oangle_sub_right, Wbtw.oangle₁₃₂_eq_zero, dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq, Sbtw.oangle_eq_left, Sbtw.oangle_sign_eq_of_sbtw_left
«term∡» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_oangle_left_toReal_lt_pi_div_two_of_dist_eq 📖	mathematical	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace	Real Real.instLT abs Real.lattice Real.instAddGroup Real.Angle.toReal oangle DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat abs_oangle_right_toReal_lt_pi_div_two_of_dist_eq oangle_eq_oangle_of_dist_eq
abs_oangle_right_toReal_lt_pi_div_two_of_dist_eq 📖	mathematical	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace	Real Real.instLT abs Real.lattice Real.instAddGroup Real.Angle.toReal oangle DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat oangle.eq_1 vsub_sub_vsub_cancel_left Orientation.abs_oangle_sub_right_toReal_lt_pi_div_two dist_eq_norm_vsub
affineIndependent_iff_of_two_zsmul_oangle_eq 📖	mathematical	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle	AffineIndependent Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Matrix.vecCons Matrix.vecEmpty	—	Real.instIsStrictOrderedRing
angle_eq_abs_oangle_toReal 📖	mathematical	—	angle abs Real Real.lattice Real.instAddGroup Real.Angle.toReal oangle	—	Real.instIsStrictOrderedRing Orientation.angle_eq_abs_oangle_toReal vsub_ne_zero
angle_eq_iff_oangle_eq_neg_of_sign_eq_neg 📖	mathematical	Real.Angle.sign oangle SignType SignType.instNeg	angle Real.Angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing Orientation.angle_eq_iff_oangle_eq_neg_of_sign_eq_neg vsub_ne_zero
angle_eq_iff_oangle_eq_of_sign_eq 📖	mathematical	Real.Angle.sign oangle	angle	—	Real.instIsStrictOrderedRing Orientation.angle_eq_iff_oangle_eq_of_sign_eq vsub_ne_zero
angle_eq_iff_oangle_eq_or_wbtw 📖	mathematical	—	angle oangle Wbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	Real.instIsStrictOrderedRing Orientation.angle_eq_iff_oangle_eq_or_sameRay vsub_ne_zero SameRay.exists_pos_left vsub_vadd one_smul wbtw_or_wbtw_smul_vadd_of_nonneg zero_le_one Real.instZeroLEOneClass LT.lt.le Wbtw.sameRay_vsub_left SameRay.symm
angle_eq_pi_div_two_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	angle	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat angle.eq_1 InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two Orientation.inner_eq_zero_of_oangle_eq_neg_pi_div_two
angle_eq_pi_div_two_of_oangle_eq_pi_div_two 📖	mathematical	oangle Real.Angle.coe Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	angle	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat angle.eq_1 InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two Orientation.inner_eq_zero_of_oangle_eq_pi_div_two
angle_rev_eq_pi_div_two_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	angle	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat angle_comm angle_eq_pi_div_two_of_oangle_eq_neg_pi_div_two
angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two 📖	mathematical	oangle Real.Angle.coe Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	angle	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat angle_comm angle_eq_pi_div_two_of_oangle_eq_pi_div_two
collinear_iff_of_two_zsmul_oangle_eq 📖	mathematical	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle	Collinear Real Real.instDivisionRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instInsert Set.instSingletonSet	—	Real.instIsStrictOrderedRing
continuousAt_oangle 📖	mathematical	—	ContinuousAt Real.Angle instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instNormedAddCommGroupAngle oangle	—	Real.instIsStrictOrderedRing ContinuousAt.comp' Orientation.continuousAt_oangle ContinuousAt.prodMk ContinuousAt.vsub instIsTopologicalAddTorsor_1 ContinuousAt.fst continuousAt_id' ContinuousAt.snd
cos_oangle_eq_cos_angle 📖	mathematical	—	Real.Angle.cos oangle Real.cos angle	—	Real.instIsStrictOrderedRing Orientation.cos_oangle_eq_cos_angle vsub_ne_zero
dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NormedAddTorsor.toAddTorsor Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike Orientation.rotation o Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing Real.Angle.coe DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup midpoint Real.instRing invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Real.instField RCLike.charZero_rclike NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Nat.instAtLeastTwoHAddOfNat RCLike.charZero_rclike vsub_midpoint vsub_sub_vsub_cancel_left inner_sub_left inner_add_right inner_smul_right real_inner_self_eq_norm_mul_norm IsStrictOrderedRing.toPosMulStrictMono IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg dist_eq_norm_vsub' real_inner_comm Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.zero_termg vsub_ne_zero Orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two eq_vadd_iff_vsub_eq dist_eq_norm_vsub vsub_vadd_eq_vsub_sub left_vsub_midpoint right_vsub_midpoint invOf_eq_inv neg_vsub_eq_vsub_rev inner_sub_sub_self smul_neg inner_self_eq_norm_sq_to_K norm_neg inner_neg_left Orientation.inner_smul_rotation_pi_div_two_smul_right sub_zero inner_neg_right Orientation.inner_smul_rotation_pi_div_two_smul_left
eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero 📖	mathematical	Real.Angle.sign oangle SignType SignType.instZero	angle Real Real.instZero Real.pi	—	Real.instIsStrictOrderedRing Orientation.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero
left_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 left_ne_of_oangle_ne_zero Real.Angle.neg_pi_div_two_ne_zero
left_ne_of_oangle_eq_pi 📖	—	oangle Real.Angle.coe Real.pi	—	—	Real.instIsStrictOrderedRing left_ne_of_oangle_ne_zero Real.Angle.pi_ne_zero
left_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 left_ne_of_oangle_ne_zero Real.Angle.pi_div_two_ne_zero
left_ne_of_oangle_ne_zero 📖	—	—	—	—	Real.instIsStrictOrderedRing vsub_ne_zero Orientation.left_ne_zero_of_oangle_ne_zero
left_ne_of_oangle_sign_eq_neg_one 📖	—	Real.Angle.sign oangle SignType SignType.instNeg SignType.instOne	—	—	Real.instIsStrictOrderedRing left_ne_of_oangle_sign_ne_zero
left_ne_of_oangle_sign_eq_one 📖	—	Real.Angle.sign oangle SignType SignType.instOne	—	—	Real.instIsStrictOrderedRing left_ne_of_oangle_sign_ne_zero
left_ne_of_oangle_sign_ne_zero 📖	—	—	—	—	Real.instIsStrictOrderedRing left_ne_of_oangle_ne_zero Real.Angle.sign_ne_zero_iff
left_ne_right_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_right_of_oangle_ne_zero Real.Angle.neg_pi_div_two_ne_zero
left_ne_right_of_oangle_eq_pi 📖	—	oangle Real.Angle.coe Real.pi	—	—	Real.instIsStrictOrderedRing left_ne_right_of_oangle_ne_zero Real.Angle.pi_ne_zero
left_ne_right_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_right_of_oangle_ne_zero Real.Angle.pi_div_two_ne_zero
left_ne_right_of_oangle_ne_zero 📖	—	—	—	—	Real.instIsStrictOrderedRing vsub_left_injective Orientation.ne_of_oangle_ne_zero
left_ne_right_of_oangle_sign_eq_neg_one 📖	—	Real.Angle.sign oangle SignType SignType.instNeg SignType.instOne	—	—	Real.instIsStrictOrderedRing left_ne_right_of_oangle_sign_ne_zero
left_ne_right_of_oangle_sign_eq_one 📖	—	Real.Angle.sign oangle SignType SignType.instOne	—	—	Real.instIsStrictOrderedRing left_ne_right_of_oangle_sign_ne_zero
left_ne_right_of_oangle_sign_ne_zero 📖	—	—	—	—	Real.instIsStrictOrderedRing left_ne_right_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 Orientation.oangle_add vsub_ne_zero
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_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 Orientation.oangle_add_oangle_rev
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 Orientation.oangle_add_swap vsub_ne_zero
oangle_eq_angle_of_sign_eq_one 📖	mathematical	Real.Angle.sign oangle SignType SignType.instOne	Real.Angle.coe angle	—	Real.instIsStrictOrderedRing Orientation.oangle_eq_angle_of_sign_eq_one
oangle_eq_angle_or_eq_neg_angle 📖	mathematical	—	oangle Real.Angle.coe angle Real.Angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing Orientation.oangle_eq_angle_or_eq_neg_angle vsub_ne_zero
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 angle	—	Real.instIsStrictOrderedRing Orientation.oangle_eq_neg_angle_of_sign_eq_neg_one
oangle_eq_neg_of_angle_eq_of_sign_eq_neg 📖	mathematical	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 Orientation.oangle_eq_neg_of_angle_eq_of_sign_eq_neg
oangle_eq_oangle_of_dist_eq 📖	mathematical	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace	oangle	—	Real.instIsStrictOrderedRing oangle.eq_1 vsub_sub_vsub_cancel_left Orientation.oangle_sub_eq_oangle_sub_rev_of_norm_eq dist_eq_norm_vsub
oangle_eq_of_angle_eq_of_sign_eq 📖	—	angle Real.Angle.sign oangle	—	—	Real.instIsStrictOrderedRing Orientation.oangle_eq_of_angle_eq_of_sign_eq
oangle_eq_of_parallel 📖	mathematical	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Set.instSingletonSet AffineSubspace.Parallel	oangle	—	Real.instIsStrictOrderedRing oangle.eq_1 Set.pair_comm AffineSubspace.direction_le affineSpan_pair_le_of_mem_of_mem exists_eq_smul_of_parallel Eq.le AffineSubspace.Parallel.direction_eq neg_vsub_eq_vsub_rev smul_neg Ne.lt_or_gt Orientation.oangle_smul_right_of_neg Orientation.oangle_smul_left_of_neg Orientation.oangle_neg_neg Orientation.oangle_smul_right_of_pos Orientation.oangle_smul_left_of_pos
oangle_eq_or_eq_neg_of_angle_eq 📖	mathematical	angle	oangle Real.Angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing oangle_eq_angle_or_eq_neg_angle neg_neg
oangle_eq_pi_iff_angle_eq_pi 📖	mathematical	—	oangle Real.Angle.coe Real.pi angle	—	Real.instIsStrictOrderedRing Orientation.oangle_eq_pi_iff_angle_eq_pi
oangle_eq_pi_iff_oangle_rev_eq_pi 📖	mathematical	—	oangle Real.Angle.coe Real.pi	—	Real.instIsStrictOrderedRing Orientation.oangle_eq_pi_iff_oangle_rev_eq_pi
oangle_eq_pi_iff_sbtw 📖	mathematical	—	oangle Real.Angle.coe Real.pi Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	Real.instIsStrictOrderedRing oangle_eq_pi_iff_angle_eq_pi angle_eq_pi_iff_sbtw
oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq 📖	mathematical	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace	oangle Real.Angle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle Real.Angle.coe Real.pi SubNegMonoid.toZSMul	—	Real.instIsStrictOrderedRing oangle.eq_1 neg_vsub_eq_vsub_rev Orientation.oangle_neg_neg Orientation.oangle_sub_eq_oangle_sub_rev_of_norm_eq dist_eq_norm_vsub Orientation.oangle.congr_simp vsub_sub_vsub_cancel_left Orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq
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 angle Real Real.instZero	—	Real.instIsStrictOrderedRing Orientation.oangle_eq_zero_iff_angle_eq_zero vsub_ne_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 Orientation.oangle_eq_zero_iff_oangle_rev_eq_zero
oangle_eq_zero_iff_wbtw 📖	mathematical	—	oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle Wbtw Real Real.instRing Real.partialOrder NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	Real.instIsStrictOrderedRing oangle.congr_simp oangle_self_left Real.instIsOrderedRing oangle_self_right oangle_eq_zero_iff_angle_eq_zero angle_eq_zero_iff_ne_and_wbtw
oangle_eq_zero_or_eq_pi_iff_collinear 📖	mathematical	—	oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle Real.Angle.coe Real.pi Collinear Real Real.instDivisionRing NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instInsert Set.instSingletonSet	—	Real.instIsStrictOrderedRing not_iff_not oangle_ne_zero_and_ne_pi_iff_affineIndependent affineIndependent_iff_not_collinear_set
oangle_homothety 📖	mathematical	—	oangle DFunLike.coe AffineMap Real CommRing.toRing Real.commRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineMap.instFunLike AffineMap.homothety	—	Real.instIsStrictOrderedRing Orientation.oangle.congr_simp smulCommClass_self AffineMap.homothety_linear Ne.lt_or_gt Orientation.oangle_smul_right_of_neg Orientation.oangle_smul_left_of_neg Orientation.oangle_neg_neg Orientation.oangle_smul_right_of_pos Orientation.oangle_smul_left_of_pos
oangle_midpoint_left 📖	mathematical	—	oangle midpoint Real Real.instRing invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Real.instField RCLike.charZero_rclike Real.instRCLike NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	Real.instIsStrictOrderedRing RCLike.charZero_rclike oangle.congr_simp midpoint_self oangle_self_left Sbtw.oangle_eq_left IsStrictOrderedRing.toCharZero Sbtw.symm Real.instIsOrderedRing sbtw_midpoint_of_ne
oangle_midpoint_rev_left 📖	mathematical	—	oangle midpoint Real Real.instRing invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Real.instField RCLike.charZero_rclike Real.instRCLike NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	Real.instIsStrictOrderedRing RCLike.charZero_rclike midpoint_comm oangle_midpoint_left
oangle_midpoint_rev_right 📖	mathematical	—	oangle midpoint Real Real.instRing invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Real.instField RCLike.charZero_rclike Real.instRCLike NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	Real.instIsStrictOrderedRing RCLike.charZero_rclike midpoint_comm oangle_midpoint_right
oangle_midpoint_right 📖	mathematical	—	oangle midpoint Real Real.instRing invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Real.instField RCLike.charZero_rclike Real.instRCLike NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	Real.instIsStrictOrderedRing RCLike.charZero_rclike oangle.congr_simp midpoint_self oangle_self_right Sbtw.oangle_eq_right IsStrictOrderedRing.toCharZero Sbtw.symm Real.instIsOrderedRing sbtw_midpoint_of_ne
oangle_ne_zero_and_ne_pi_iff_affineIndependent 📖	mathematical	—	AffineIndependent Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Matrix.vecCons Matrix.vecEmpty	—	Real.instIsStrictOrderedRing oangle.eq_1 Orientation.oangle_ne_zero_and_ne_pi_iff_linearIndependent affineIndependent_iff_linearIndependent_vsub linearIndependent_equiv Fintype.complete
oangle_ne_zero_and_ne_pi_iff_not_collinear 📖	mathematical	—	Collinear Real Real.instDivisionRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instInsert Set.instSingletonSet	—	Real.instIsStrictOrderedRing oangle_ne_zero_and_ne_pi_iff_affineIndependent affineIndependent_iff_not_collinear_set
oangle_rev 📖	mathematical	—	oangle Real.Angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing Orientation.oangle_rev
oangle_rotate_sign 📖	mathematical	—	Real.Angle.sign oangle	—	Real.instIsStrictOrderedRing oangle_swap₁₂_sign oangle_swap₁₃_sign
oangle_self_left 📖	mathematical	—	oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing Orientation.oangle.congr_simp vsub_self Orientation.oangle_zero_left
oangle_self_left_right 📖	mathematical	—	oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing Orientation.oangle_self
oangle_self_right 📖	mathematical	—	oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing Orientation.oangle.congr_simp vsub_self Orientation.oangle_zero_right
oangle_sign_eq_zero_iff_collinear 📖	mathematical	—	Real.Angle.sign oangle SignType SignType.instZero Collinear Real Real.instDivisionRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instInsert Set.instSingletonSet	—	Real.instIsStrictOrderedRing Real.Angle.sign_eq_zero_iff oangle_eq_zero_or_eq_pi_iff_collinear
oangle_sub_left 📖	mathematical	—	Real.Angle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle	—	Real.instIsStrictOrderedRing Orientation.oangle_sub_left vsub_ne_zero
oangle_sub_right 📖	mathematical	—	Real.Angle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle	—	Real.instIsStrictOrderedRing Orientation.oangle_sub_right vsub_ne_zero
oangle_swap₁₂_sign 📖	mathematical	—	SignType SignType.instNeg Real.Angle.sign oangle	—	Real.instIsStrictOrderedRing oangle.eq_1 Orientation.oangle_neg_neg neg_vsub_eq_vsub_rev vsub_sub_vsub_cancel_left sub_eq_add_neg add_comm neg_one_smul one_smul Orientation.oangle_sign_smul_add_smul_right sign_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike neg_mul one_mul
oangle_swap₁₃_sign 📖	mathematical	—	SignType SignType.instNeg Real.Angle.sign oangle	—	Real.instIsStrictOrderedRing oangle_rev Real.Angle.sign_neg neg_neg
oangle_swap₂₃_sign 📖	mathematical	—	SignType SignType.instNeg Real.Angle.sign oangle	—	Real.instIsStrictOrderedRing oangle_swap₁₃_sign oangle_swap₁₂_sign
right_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 right_ne_of_oangle_ne_zero Real.Angle.neg_pi_div_two_ne_zero
right_ne_of_oangle_eq_pi 📖	—	oangle Real.Angle.coe Real.pi	—	—	Real.instIsStrictOrderedRing right_ne_of_oangle_ne_zero Real.Angle.pi_ne_zero
right_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 right_ne_of_oangle_ne_zero Real.Angle.pi_div_two_ne_zero
right_ne_of_oangle_ne_zero 📖	—	—	—	—	Real.instIsStrictOrderedRing vsub_ne_zero Orientation.right_ne_zero_of_oangle_ne_zero
right_ne_of_oangle_sign_eq_neg_one 📖	—	Real.Angle.sign oangle SignType SignType.instNeg SignType.instOne	—	—	Real.instIsStrictOrderedRing right_ne_of_oangle_sign_ne_zero
right_ne_of_oangle_sign_eq_one 📖	—	Real.Angle.sign oangle SignType SignType.instOne	—	—	Real.instIsStrictOrderedRing right_ne_of_oangle_sign_ne_zero
right_ne_of_oangle_sign_ne_zero 📖	—	—	—	—	Real.instIsStrictOrderedRing right_ne_of_oangle_ne_zero Real.Angle.sign_ne_zero_iff
two_zsmul_oangle_of_parallel 📖	mathematical	AffineSubspace.Parallel Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace affineSpan Set Set.instInsert Set.instSingletonSet	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle	—	Real.instIsStrictOrderedRing two_zsmul_oangle_of_vectorSpan_eq AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq
two_zsmul_oangle_of_vectorSpan_eq 📖	mathematical	vectorSpan Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instInsert Set.instSingletonSet	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle	—	Real.instIsStrictOrderedRing Orientation.two_zsmul_oangle_of_span_eq_of_span_eq vectorSpan_pair

Sbtw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
oangle_eq_add_pi_left 📖	mathematical	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.oangle Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.Angle.coe Real.pi	—	Real.instIsStrictOrderedRing oangle₁₂₃_eq_pi EuclideanGeometry.oangle_add_swap left_ne right_ne
oangle_eq_add_pi_right 📖	mathematical	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.oangle Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.Angle.coe Real.pi	—	Real.instIsStrictOrderedRing oangle₃₂₁_eq_pi EuclideanGeometry.oangle_add right_ne left_ne
oangle_eq_left 📖	mathematical	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.oangle	—	Real.instIsStrictOrderedRing Wbtw.oangle_eq_left wbtw ne_left
oangle_eq_left_right 📖	mathematical	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.oangle	—	Real.instIsStrictOrderedRing oangle_eq_add_pi_left left_ne oangle_eq_add_pi_right right_ne add_assoc Real.Angle.coe_pi_add_coe_pi add_zero
oangle_eq_right 📖	mathematical	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.oangle	—	Real.instIsStrictOrderedRing Wbtw.oangle_eq_right wbtw ne_left
oangle_sign_eq 📖	mathematical	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	Real.Angle.sign EuclideanGeometry.oangle	—	Real.instIsStrictOrderedRing Collinear.oangle_sign_of_sameRay_vsub left_ne ne_right Set.insert_eq_of_mem Wbtw.collinear wbtw Wbtw.sameRay_vsub
oangle_sign_eq_left 📖	mathematical	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	Real.Angle.sign EuclideanGeometry.oangle	—	Real.instIsStrictOrderedRing Wbtw.oangle_sign_eq_of_ne_left wbtw left_ne
oangle_sign_eq_of_sbtw 📖	mathematical	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	Real.Angle.sign EuclideanGeometry.oangle	—	Real.instIsStrictOrderedRing oangle_eq_right symm Real.instIsOrderedRing oangle_sign_eq EuclideanGeometry.oangle_rotate_sign oangle_eq_left
oangle_sign_eq_of_sbtw_left 📖	mathematical	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	Real.Angle.sign EuclideanGeometry.oangle	—	Real.instIsStrictOrderedRing oangle_eq_right symm Real.instIsOrderedRing oangle_sign_eq_right EuclideanGeometry.oangle_rotate_sign oangle_sign_eq_left oangle_eq_left
oangle_sign_eq_right 📖	mathematical	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	Real.Angle.sign EuclideanGeometry.oangle	—	Real.instIsStrictOrderedRing Wbtw.oangle_sign_eq_of_ne_right wbtw ne_right
oangle₁₂₃_eq_pi 📖	mathematical	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.oangle Real.Angle.coe Real.pi	—	Real.instIsStrictOrderedRing EuclideanGeometry.oangle_eq_pi_iff_sbtw
oangle₁₃₂_eq_zero 📖	mathematical	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing Wbtw.oangle₁₃₂_eq_zero wbtw
oangle₂₁₃_eq_zero 📖	mathematical	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing Wbtw.oangle₂₁₃_eq_zero wbtw
oangle₂₃₁_eq_zero 📖	mathematical	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing Wbtw.oangle₂₃₁_eq_zero wbtw
oangle₃₁₂_eq_zero 📖	mathematical	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing Wbtw.oangle₃₁₂_eq_zero wbtw
oangle₃₂₁_eq_pi 📖	mathematical	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.oangle Real.Angle.coe Real.pi	—	Real.instIsStrictOrderedRing EuclideanGeometry.oangle_eq_pi_iff_oangle_rev_eq_pi oangle₁₂₃_eq_pi

Wbtw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
oangle_eq_left 📖	mathematical	Wbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.oangle	—	Real.instIsStrictOrderedRing EuclideanGeometry.oangle.congr_simp EuclideanGeometry.oangle_self_right wbtw_self_iff Real.instIsOrderedRing EuclideanGeometry.oangle_add oangle₃₁₂_eq_zero zero_add
oangle_eq_right 📖	mathematical	Wbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.oangle	—	Real.instIsStrictOrderedRing EuclideanGeometry.oangle_rev oangle_eq_left
oangle_sign_eq_of_ne_left 📖	mathematical	Wbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	Real.Angle.sign EuclideanGeometry.oangle	—	Real.instIsStrictOrderedRing Collinear.oangle_sign_of_sameRay_vsub left_ne_right_of_ne_left Real.instIsOrderedRing Set.insert_comm Set.insert_eq_of_mem collinear sameRay_vsub_left
oangle_sign_eq_of_ne_right 📖	mathematical	Wbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	Real.Angle.sign EuclideanGeometry.oangle	—	Real.instIsStrictOrderedRing EuclideanGeometry.oangle_rev Real.Angle.sign_neg oangle_sign_eq_of_ne_left symm Real.instIsOrderedRing
oangle₁₃₂_eq_zero 📖	mathematical	Wbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing oangle₃₁₂_eq_zero symm Real.instIsOrderedRing
oangle₂₁₃_eq_zero 📖	mathematical	Wbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing EuclideanGeometry.oangle.congr_simp EuclideanGeometry.oangle_self_left EuclideanGeometry.oangle_self_right EuclideanGeometry.oangle_eq_zero_iff_angle_eq_zero angle₂₁₃_eq_zero_of_ne
oangle₂₃₁_eq_zero 📖	mathematical	Wbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing oangle₂₁₃_eq_zero symm Real.instIsOrderedRing
oangle₃₁₂_eq_zero 📖	mathematical	Wbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.oangle Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing EuclideanGeometry.oangle_eq_zero_iff_oangle_rev_eq_zero oangle₂₁₃_eq_zero

---

← Back to Index