Affine

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

Statistics

Metric	Count
Definitions angle, «term∠»	2
Theorems angle_map, angle_coe, angle_add_angle_eq_pi_of_angle_eq_pi, angle_add_const, angle_comm, angle_const_add, angle_const_sub, angle_const_vadd, angle_const_vsub, angle_eq_angle_of_angle_eq_pi, angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi, angle_eq_pi_iff_sbtw, angle_eq_zero_iff_eq_and_ne_or_sbtw, angle_eq_zero_iff_ne_and_wbtw, angle_eq_zero_of_angle_eq_pi_left, angle_eq_zero_of_angle_eq_pi_right, angle_homothety, angle_le_pi, angle_left_midpoint_eq_pi_div_two_of_dist_eq, angle_lt_pi_of_not_collinear, angle_midpoint_eq_pi, angle_ne_pi_of_not_collinear, angle_ne_zero_of_not_collinear, angle_neg, angle_nonneg, angle_pos_of_not_collinear, angle_right_midpoint_eq_pi_div_two_of_dist_eq, angle_self_left, angle_self_of_ne, angle_self_right, angle_sub_const, angle_vadd_const, angle_vsub_const, collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi, collinear_iff_eq_or_eq_or_sin_eq_zero, collinear_of_angle_eq_pi, collinear_of_angle_eq_zero, collinear_of_sin_eq_zero, continuousAt_angle, cos_eq_neg_one_iff_angle_eq_pi, cos_eq_one_iff_angle_eq_zero, cos_eq_zero_iff_angle_eq_pi_div_two, dist_eq_abs_sub_dist_iff_angle_eq_zero, dist_eq_abs_sub_dist_of_angle_eq_zero, dist_eq_add_dist_iff_angle_eq_pi, dist_eq_add_dist_of_angle_eq_pi, left_dist_ne_zero_of_angle_eq_pi, right_dist_ne_zero_of_angle_eq_pi, sin_eq_one_iff_angle_eq_pi_div_two, sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi, sin_ne_zero_of_not_collinear, sin_pos_of_not_collinear, angle_eq_left, angle_eq_right, angle₁₂₃_eq_pi, angle₁₃₂_eq_zero, angle₂₁₃_eq_zero, angle₂₃₁_eq_zero, angle₃₁₂_eq_zero, angle₃₂₁_eq_pi, angle_eq_left, angle_eq_right, angle₁₃₂_eq_zero_of_ne, angle₂₁₃_eq_zero_of_ne, angle₂₃₁_eq_zero_of_ne, angle₃₁₂_eq_zero_of_ne	66
Total	68

AffineIsometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
angle_map 📖	mathematical	—	EuclideanGeometry.angle DFunLike.coe AffineIsometry Real Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike MetricSpace.toPseudoMetricSpace instFunLike	—	LinearIsometry.angle_map

AffineSubspace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
angle_coe 📖	mathematical	—	EuclideanGeometry.angle AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership instSetLike Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Submodule.setLike direction Submodule.normedAddCommGroup Submodule.innerProductSpace Subtype.metricSpace toNormedAddTorsor	—	AffineIsometry.angle_map

EuclideanGeometry

Definitions

Name	Category	Theorems
angle 📖	CompOp	95 math math: Sphere.thales_theorem, angle_comm, eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero, Sbtw.angle₁₃₂_eq_zero, angle_le_pi, law_sin, oangle_eq_angle_or_eq_neg_angle, dist_eq_add_dist_iff_angle_eq_pi, angle_eq_iff_oangle_eq_or_wbtw, angle_vadd_const, Similar.angle_eq, angle_self_of_ne, Sbtw.angle₃₁₂_eq_zero, angle_eq_zero_iff_eq_and_ne_or_sbtw, angle_orthogonalProjection_self, angle_eq_pi_div_two_of_oangle_eq_neg_pi_div_two, angle_le_iff_dist_le, angle_pos_of_not_collinear, dist_orthogonalProjection_eq_iff_angle_eq, oangle_eq_zero_iff_angle_eq_zero, Affine.Triangle.dist_div_sin_angle_eq_two_mul_circumradius, Sphere.IsTangentAt.angle_eq_pi_div_two, angle_vsub_const, dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle, angle_le_angle_add_angle, angle_eq_iff_oangle_eq_of_sign_eq, angle_self_right, angle_add_const, angle_eq_pi_div_two_of_oangle_eq_pi_div_two, Affine.Triangle.acuteAngled_iff_angle_lt, sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi, oangle_eq_pi_iff_angle_eq_pi, angle_lt_iff_dist_lt, cos_oangle_eq_cos_angle, Wbtw.angle₃₁₂_eq_zero_of_ne, exterior_angle_eq_angle_add_angle, sin_eq_one_iff_angle_eq_pi_div_two, dist_eq_abs_sub_dist_iff_angle_eq_zero, sin_angle_div_dist_eq_sin_angle_div_dist, angle_const_add, angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two, continuousAt_angle, Sbtw.angle₁₂₃_eq_pi, cos_eq_neg_one_iff_angle_eq_pi, Sbtw.angle_eq_right, collinear_iff_eq_or_eq_or_sin_eq_zero, angle_sub_const, sin_angle_mul_dist_eq_sin_angle_mul_dist, Sbtw.angle₂₃₁_eq_zero, angle_homothety, Wbtw.angle₁₃₂_eq_zero_of_ne, dist_eq_dist_mul_sin_angle_div_sin_angle, angle_eq_of_congruent, angle_add_of_ne_of_ne, angle_eq_iff_oangle_eq_neg_of_sign_eq_neg, Wbtw.angle₂₁₃_eq_zero_of_ne, cos_eq_zero_iff_angle_eq_pi_div_two, angle_left_midpoint_eq_pi_div_two_of_dist_eq, Wbtw.angle₂₃₁_eq_zero_of_ne, angle_eq_abs_oangle_toReal, Sbtw.angle₃₂₁_eq_pi, angle_const_vsub, Sbtw.angle_eq_left, angle_midpoint_eq_pi, Wbtw.angle_eq_right, collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi, oangle_eq_angle_of_sign_eq_one, Sbtw.angle₂₁₃_eq_zero, angle_neg, Sphere.IsTangentAt_iff_angle_eq_pi_div_two, Wbtw.angle_eq_left, Affine.Triangle.dist_div_sin_angle_div_two_eq_circumradius, angle_const_sub, law_cos, angle_self_orthogonalProjection, AffineSubspace.angle_coe, angle_right_midpoint_eq_pi_div_two_of_dist_eq, angle_nonneg, Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter, angle_eq_zero_iff_ne_and_wbtw, Affine.Simplex.Equilateral.angle_eq_pi_div_three, cos_eq_one_iff_angle_eq_zero, sin_pos_of_not_collinear, Sphere.angle_eq_pi_div_two_iff_mem_sphere_ofDiameter, angle_lt_pi_of_not_collinear, angle_self_left, oangle_eq_neg_angle_of_sign_eq_neg_one, Similar.angle_eq_all, AffineIsometry.angle_map, dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two, angle_add_angle_add_angle_eq_pi, angle_rev_eq_pi_div_two_of_oangle_eq_neg_pi_div_two, angle_eq_angle_of_dist_eq, angle_eq_pi_iff_sbtw, angle_const_vadd
«term∠» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
angle_add_angle_eq_pi_of_angle_eq_pi 📖	mathematical	angle Real.pi	Real Real.instAdd	—	angle_comm InnerProductGeometry.angle_add_angle_eq_pi_of_angle_eq_pi
angle_add_const 📖	mathematical	—	angle NormedAddCommGroup.toMetricSpace SeminormedAddCommGroup.toNormedAddTorsor NormedAddCommGroup.toSeminormedAddCommGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	angle_vadd_const
angle_comm 📖	mathematical	—	angle	—	InnerProductGeometry.angle_comm
angle_const_add 📖	mathematical	—	angle NormedAddCommGroup.toMetricSpace SeminormedAddCommGroup.toNormedAddTorsor NormedAddCommGroup.toSeminormedAddCommGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	angle_const_vadd
angle_const_sub 📖	mathematical	—	angle NormedAddCommGroup.toMetricSpace SeminormedAddCommGroup.toNormedAddTorsor NormedAddCommGroup.toSeminormedAddCommGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	angle_const_vsub
angle_const_vadd 📖	mathematical	—	angle 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 MetricSpace.toPseudoMetricSpace	—	AffineIsometry.angle_map
angle_const_vsub 📖	mathematical	—	angle NormedAddCommGroup.toMetricSpace SeminormedAddCommGroup.toNormedAddTorsor NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	AffineIsometry.angle_map
angle_eq_angle_of_angle_eq_pi 📖	—	angle Real.pi	—	—	InnerProductGeometry.angle_eq_pi_iff add_smul neg_vsub_eq_vsub_rev smul_neg neg_smul one_smul vsub_add_vsub_cancel InnerProductGeometry.angle_smul_right_of_pos add_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid neg_pos_of_neg zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi 📖	—	angle Real.pi	—	—	Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing neg_eq_zero sub_eq_zero_of_eq angle_add_angle_eq_pi_of_angle_eq_pi angle_comm
angle_eq_pi_iff_sbtw 📖	mathematical	—	angle Real.pi Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	angle.eq_1 InnerProductGeometry.angle_eq_pi_iff div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing zero_le_one Real.instZeroLEOneClass sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LE.le.trans LT.lt.le div_le_one sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd LT.lt.trans zero_lt_one NeZero.charZero_one RCLike.charZero_rclike le_sub_self_iff AffineMap.lineMap_apply eq_vadd_iff_vsub_eq vadd_vsub_assoc neg_vsub_eq_vsub_rev smul_neg neg_smul smul_add smul_smul add_smul Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add mul_neg Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.subst_sub one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg LT.lt.ne Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add one_smul vsub_ne_zero smul_ne_zero_iff instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Real.instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero Sbtw.angle₁₂₃_eq_pi
angle_eq_zero_iff_eq_and_ne_or_sbtw 📖	mathematical	—	angle Real Real.instZero Sbtw Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	angle_eq_zero_iff_ne_and_wbtw Real.instIsOrderedRing
angle_eq_zero_iff_ne_and_wbtw 📖	mathematical	—	angle Real Real.instZero Wbtw Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	angle.eq_1 InnerProductGeometry.angle_eq_zero_iff le_or_gt vsub_ne_zero LT.lt.le inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing inv_le_one_of_one_le₀ Real.instZeroLEOneClass AffineMap.lineMap_apply smul_smul inv_mul_cancel₀ LT.lt.ne one_smul vsub_vadd smul_ne_zero_iff instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Real.instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero Wbtw.angle₂₁₃_eq_zero_of_ne Wbtw.angle₃₁₂_eq_zero_of_ne
angle_eq_zero_of_angle_eq_pi_left 📖	mathematical	angle Real.pi	Real Real.instZero	—	InnerProductGeometry.angle_eq_pi_iff InnerProductGeometry.angle_eq_zero_iff neg_ne_zero neg_vsub_eq_vsub_rev add_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid neg_pos_of_neg zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike add_smul smul_neg neg_smul one_smul vsub_add_vsub_cancel
angle_eq_zero_of_angle_eq_pi_right 📖	mathematical	angle Real.pi	Real Real.instZero	—	angle_eq_zero_of_angle_eq_pi_left angle_comm
angle_homothety 📖	mathematical	—	angle 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	—	smulCommClass_self AffineMap.homothety_linear Ne.lt_or_gt InnerProductGeometry.angle_smul_right_of_neg InnerProductGeometry.angle_smul_left_of_neg InnerProductGeometry.angle_neg_neg InnerProductGeometry.angle_smul_right_of_pos InnerProductGeometry.angle_smul_left_of_pos
angle_le_pi 📖	mathematical	—	Real Real.instLE angle Real.pi	—	InnerProductGeometry.angle_le_pi
angle_left_midpoint_eq_pi_div_two_of_dist_eq 📖	mathematical	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace	angle 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 DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	RCLike.charZero_rclike vsub_sub_vsub_cancel_right Nat.instAtLeastTwoHAddOfNat left_vsub_midpoint midpoint_vsub_right vsub_add_vsub_cancel InnerProductGeometry.norm_add_eq_norm_sub_iff_angle_eq_pi_div_two dist_eq_norm_vsub
angle_lt_pi_of_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.instLT angle Real.pi	—	LE.le.lt_of_ne angle_le_pi angle_ne_pi_of_not_collinear
angle_midpoint_eq_pi 📖	mathematical	—	angle 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.pi	—	RCLike.charZero_rclike Nat.instAtLeastTwoHAddOfNat left_vsub_midpoint invOf_eq_inv right_vsub_midpoint InnerProductGeometry.angle_smul_right_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass NeZero.charZero_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid InnerProductGeometry.angle_smul_left_of_pos neg_vsub_eq_vsub_rev InnerProductGeometry.angle_self_neg_of_nonzero
angle_ne_pi_of_not_collinear 📖	—	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	—	—	collinear_of_angle_eq_pi
angle_ne_zero_of_not_collinear 📖	—	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	—	—	collinear_of_angle_eq_zero
angle_neg 📖	mathematical	—	angle NormedAddCommGroup.toMetricSpace SeminormedAddCommGroup.toNormedAddTorsor NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	zero_sub angle_const_sub
angle_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero angle	—	InnerProductGeometry.angle_nonneg
angle_pos_of_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.instLT Real.instZero angle	—	LE.le.lt_of_ne angle_nonneg angle_ne_zero_of_not_collinear
angle_right_midpoint_eq_pi_div_two_of_dist_eq 📖	mathematical	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace	angle 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 DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	RCLike.charZero_rclike Nat.instAtLeastTwoHAddOfNat midpoint_comm angle_left_midpoint_eq_pi_div_two_of_dist_eq
angle_self_left 📖	mathematical	—	angle Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat vsub_self InnerProductGeometry.angle_zero_left
angle_self_of_ne 📖	mathematical	—	angle Real Real.instZero	—	InnerProductGeometry.angle_self vsub_ne_zero
angle_self_right 📖	mathematical	—	angle Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat angle_comm angle_self_left
angle_sub_const 📖	mathematical	—	angle NormedAddCommGroup.toMetricSpace SeminormedAddCommGroup.toNormedAddTorsor NormedAddCommGroup.toSeminormedAddCommGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	angle_vsub_const
angle_vadd_const 📖	mathematical	—	angle 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 MetricSpace.toPseudoMetricSpace NormedAddCommGroup.toMetricSpace SeminormedAddCommGroup.toNormedAddTorsor	—	AffineIsometry.angle_map
angle_vsub_const 📖	mathematical	—	angle NormedAddCommGroup.toMetricSpace SeminormedAddCommGroup.toNormedAddTorsor NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	AffineIsometry.angle_map
collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi 📖	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 angle Real.instZero Real.pi	—	Collinear.wbtw_or_wbtw_or_wbtw Real.instIsStrictOrderedRing angle_eq_pi_iff_sbtw Wbtw.angle₃₁₂_eq_zero_of_ne Wbtw.angle₂₃₁_eq_zero_of_ne Set.insert_eq_of_mem collinear_pair angle_eq_zero_iff_ne_and_wbtw Set.insert_comm Wbtw.collinear Set.pair_comm Sbtw.wbtw
collinear_iff_eq_or_eq_or_sin_eq_zero 📖	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.sin angle Real.instZero	—	sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi
collinear_of_angle_eq_pi 📖	mathematical	angle Real.pi	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	—	collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi
collinear_of_angle_eq_zero 📖	mathematical	angle Real Real.instZero	Collinear Real.instDivisionRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instInsert Set.instSingletonSet	—	collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi
collinear_of_sin_eq_zero 📖	mathematical	Real.sin angle Real Real.instZero	Collinear Real.instDivisionRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instInsert Set.instSingletonSet	—	Mathlib.Tactic.Contrapose.contrapose₁ sin_ne_zero_of_not_collinear
continuousAt_angle 📖	mathematical	—	ContinuousAt Real instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Real.pseudoMetricSpace angle	—	ContinuousAt.comp InnerProductGeometry.continuousAt_angle ContinuousAt.prodMk ContinuousAt.vsub instIsTopologicalAddTorsor_1 ContinuousAt.fst continuousAt_id' ContinuousAt.snd
cos_eq_neg_one_iff_angle_eq_pi 📖	mathematical	—	Real.cos angle Real Real.instNeg Real.instOne Real.pi	—	InnerProductGeometry.cos_eq_neg_one_iff_angle_eq_pi
cos_eq_one_iff_angle_eq_zero 📖	mathematical	—	Real.cos angle Real Real.instOne Real.instZero	—	InnerProductGeometry.cos_eq_one_iff_angle_eq_zero
cos_eq_zero_iff_angle_eq_pi_div_two 📖	mathematical	—	Real.cos angle Real Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	InnerProductGeometry.cos_eq_zero_iff_angle_eq_pi_div_two
dist_eq_abs_sub_dist_iff_angle_eq_zero 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace abs Real Real.lattice Real.instAddGroup Real.instSub angle Real.instZero	—	dist_eq_norm_vsub vsub_sub_vsub_cancel_right InnerProductGeometry.norm_sub_eq_abs_sub_norm_iff_angle_eq_zero vsub_eq_zero_iff_eq
dist_eq_abs_sub_dist_of_angle_eq_zero 📖	mathematical	angle Real Real.instZero	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace abs Real.lattice Real.instAddGroup Real.instSub	—	dist_eq_norm_vsub vsub_sub_vsub_cancel_right InnerProductGeometry.norm_sub_eq_abs_sub_norm_of_angle_eq_zero
dist_eq_add_dist_iff_angle_eq_pi 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Real Real.instAdd angle Real.pi	—	dist_eq_norm_vsub vsub_sub_vsub_cancel_right InnerProductGeometry.norm_sub_eq_add_norm_iff_angle_eq_pi vsub_eq_zero_iff_eq
dist_eq_add_dist_of_angle_eq_pi 📖	mathematical	angle Real.pi	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Real Real.instAdd	—	dist_eq_norm_vsub vsub_sub_vsub_cancel_right InnerProductGeometry.norm_sub_eq_add_norm_of_angle_eq_pi
left_dist_ne_zero_of_angle_eq_pi 📖	—	angle Real.pi	—	—	Real.pi_ne_zero Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Linarith.lt_of_eq_of_lt Nat.instAtLeastTwoHAddOfNat CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_eq Real.instIsOrderedRing sub_eq_zero_of_eq angle_self_left dist_eq_zero Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq neg_eq_zero
right_dist_ne_zero_of_angle_eq_pi 📖	—	angle Real.pi	—	—	left_dist_ne_zero_of_angle_eq_pi angle_comm
sin_eq_one_iff_angle_eq_pi_div_two 📖	mathematical	—	Real.sin angle Real Real.instOne DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	InnerProductGeometry.sin_eq_one_iff_angle_eq_pi_div_two
sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi 📖	mathematical	—	Real.sin angle Real Real.instZero Real.pi	—	InnerProductGeometry.sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi
sin_ne_zero_of_not_collinear 📖	—	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	—	—	ne_of_gt sin_pos_of_not_collinear
sin_pos_of_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.instLT Real.instZero Real.sin angle	—	Real.sin_pos_of_pos_of_lt_pi angle_pos_of_not_collinear angle_lt_pi_of_not_collinear

Sbtw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
angle_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.angle	—	EuclideanGeometry.angle_comm angle_eq_right
angle_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.angle	—	EuclideanGeometry.angle_eq_angle_of_angle_eq_pi angle₁₂₃_eq_pi
angle₁₂₃_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.angle Real.pi	—	EuclideanGeometry.angle.eq_1 InnerProductGeometry.angle_eq_pi_iff vsub_ne_zero AffineMap.lineMap_apply_zero AffineMap.lineMap_apply_one LE.le.lt_of_ne div_neg_of_neg_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Left.neg_neg_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add AffineMap.lineMap_apply vsub_vadd_eq_vsub_sub vsub_self zero_sub smul_neg smul_smul div_mul_cancel₀ neg_smul neg_neg sub_eq_iff_eq_add add_smul sub_add_cancel one_smul
angle₁₃₂_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.angle Real.instZero	—	Wbtw.angle₁₃₂_eq_zero_of_ne wbtw ne_right
angle₂₁₃_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.angle Real.instZero	—	Wbtw.angle₂₁₃_eq_zero_of_ne wbtw ne_left
angle₂₃₁_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.angle Real.instZero	—	Wbtw.angle₂₃₁_eq_zero_of_ne wbtw ne_right
angle₃₁₂_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.angle Real.instZero	—	Wbtw.angle₃₁₂_eq_zero_of_ne wbtw ne_left
angle₃₂₁_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.angle Real.pi	—	angle₁₂₃_eq_pi EuclideanGeometry.angle_comm

Wbtw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
angle_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.angle	—	EuclideanGeometry.angle_comm angle_eq_right
angle_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.angle	—	Sbtw.angle_eq_right
angle₁₃₂_eq_zero_of_ne 📖	mathematical	Wbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.angle Real.instZero	—	angle₃₁₂_eq_zero_of_ne symm Real.instIsOrderedRing
angle₂₁₃_eq_zero_of_ne 📖	mathematical	Wbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.angle Real.instZero	—	EuclideanGeometry.angle.eq_1 InnerProductGeometry.angle_eq_zero_iff AffineMap.lineMap_apply_zero LE.le.lt_of_ne vsub_ne_zero inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing AffineMap.lineMap_apply vadd_vsub_assoc vsub_self add_zero smul_smul inv_mul_cancel₀ one_smul
angle₂₃₁_eq_zero_of_ne 📖	mathematical	Wbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.angle Real.instZero	—	angle₂₁₃_eq_zero_of_ne symm Real.instIsOrderedRing
angle₃₁₂_eq_zero_of_ne 📖	mathematical	Wbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.angle Real.instZero	—	angle₂₁₃_eq_zero_of_ne EuclideanGeometry.angle_comm

---

← Back to Index