Sphere

📁 Source: Mathlib/Geometry/Euclidean/Angle/Sphere.lean

Statistics

Metric	Count
Definitions	0
Theorems circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq, circumsphere_eq_of_dist_of_oangle, dist_div_sin_angle_div_two_eq_circumradius, dist_div_sin_angle_eq_two_mul_circumradius, dist_div_sin_oangle_div_two_eq_circumradius, dist_div_sin_oangle_eq_two_mul_circumradius, inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter, mem_circumsphere_of_two_zsmul_oangle_eq, two_zsmul_oangle_eq, angle_eq_pi_div_two, IsTangentAt_iff_angle_eq_pi_div_two, IsTangentAt_of_angle_eq_pi_div_two, abs_oangle_center_left_toReal_lt_pi_div_two, abs_oangle_center_right_toReal_lt_pi_div_two, angle_eq_pi_div_two_iff_mem_sphere_ofDiameter, angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter, dist_div_cos_oangle_center_div_two_eq_radius, dist_div_cos_oangle_center_eq_two_mul_radius, dist_div_sin_oangle_div_two_eq_radius, dist_div_sin_oangle_eq_two_mul_radius, inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, isDiameter_of_angle_eq_pi_div_two, oangle_center_eq_two_zsmul_oangle, oangle_eq_pi_sub_two_zsmul_oangle_center_left, oangle_eq_pi_sub_two_zsmul_oangle_center_right, tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, thales_theorem, two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi, two_zsmul_oangle_eq, concyclic_of_two_zsmul_oangle_eq_of_not_collinear, concyclic_or_collinear_of_two_zsmul_oangle_eq, cospherical_of_two_zsmul_oangle_eq_of_not_collinear, cospherical_or_collinear_of_two_zsmul_oangle_eq, oangle_eq_two_zsmul_oangle_sub_of_norm_eq, oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real, two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq	36
Total	36

Affine.Triangle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq 📖	mathematical	Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle EuclideanGeometry.oangle	Affine.Simplex.circumsphere	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids RCLike.charZero_rclike circumsphere_eq_of_dist_of_oangle Real.Angle.tan_eq_of_two_zsmul_eq Real.Angle.abs_sin_eq_of_two_zsmul_eq
circumsphere_eq_of_dist_of_oangle 📖	mathematical	—	Affine.Simplex.circumsphere 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 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 DivInvMonoid.toDiv Real.instDivInvMonoid Real.instInv Real.Angle.tan EuclideanGeometry.oangle Affine.Simplex.points Real.instRing NormedAddCommGroup.toAddCommGroup instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike Orientation.rotation EuclideanGeometry.o Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing Real.Angle.coe Real.pi VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup midpoint invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Real.instField RCLike.charZero_rclike Dist.dist PseudoMetricSpace.toDist abs Real.lattice Real.instAddGroup Real.Angle.sin	—	Real.instIsStrictOrderedRing EuclideanGeometry.Sphere.ext Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids RCLike.charZero_rclike inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter dist_div_sin_oangle_div_two_eq_circumradius
dist_div_sin_angle_div_two_eq_circumradius 📖	mathematical	—	Real DivInvMonoid.toDiv Real.instDivInvMonoid Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Affine.Simplex.points Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor Real.sin EuclideanGeometry.angle instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Affine.Simplex.circumradius	—	instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange le_rfl direction_affineSpan AffineIndependent.finrank_vectorSpan Affine.Simplex.independent Fintype.card_fin Real.instIsStrictOrderedRing commRing_strongRankCondition Real.instNontrivial Module.Free.of_divisionRing finiteDimensional_direction_affineSpan_range Finite.of_fintype Fact.out Nat.instAtLeastTwoHAddOfNat Real.Angle.sin_toReal Real.abs_sin_eq_sin_abs_of_abs_le_pi Real.Angle.abs_toReal_le_pi EuclideanGeometry.angle_eq_abs_oangle_toReal AffineIndependent.injective Affine.Simplex.circumradius_restrict dist_div_sin_oangle_div_two_eq_circumradius
dist_div_sin_angle_eq_two_mul_circumradius 📖	mathematical	—	Real DivInvMonoid.toDiv Real.instDivInvMonoid Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Affine.Simplex.points Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor Real.sin EuclideanGeometry.angle Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Affine.Simplex.circumradius	—	Nat.instAtLeastTwoHAddOfNat dist_div_sin_angle_div_two_eq_circumradius Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz
dist_div_sin_oangle_div_two_eq_circumradius 📖	mathematical	—	Real DivInvMonoid.toDiv Real.instDivInvMonoid Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Affine.Simplex.points Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor abs Real.lattice Real.instAddGroup Real.Angle.sin EuclideanGeometry.oangle instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Affine.Simplex.circumradius	—	Real.instIsStrictOrderedRing EuclideanGeometry.Sphere.dist_div_sin_oangle_div_two_eq_radius Affine.Simplex.mem_circumsphere AffineIndependent.injective Real.instNontrivial Affine.Simplex.independent
dist_div_sin_oangle_eq_two_mul_circumradius 📖	mathematical	—	Real DivInvMonoid.toDiv Real.instDivInvMonoid Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Affine.Simplex.points Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor abs Real.lattice Real.instAddGroup Real.Angle.sin EuclideanGeometry.oangle Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Affine.Simplex.circumradius	—	Real.instIsStrictOrderedRing EuclideanGeometry.Sphere.dist_div_sin_oangle_eq_two_mul_radius Affine.Simplex.mem_circumsphere AffineIndependent.injective Real.instNontrivial Affine.Simplex.independent
inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter 📖	mathematical	—	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 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 DivInvMonoid.toDiv Real.instDivInvMonoid Real.instInv Real.Angle.tan EuclideanGeometry.oangle Affine.Simplex.points Real.instRing NormedAddCommGroup.toAddCommGroup instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike Orientation.rotation EuclideanGeometry.o Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing Real.Angle.coe Real.pi VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup midpoint invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Real.instField RCLike.charZero_rclike Affine.Simplex.circumcenter	—	Real.instIsStrictOrderedRing EuclideanGeometry.Sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center Affine.Simplex.mem_circumsphere AffineIndependent.injective Real.instNontrivial Affine.Simplex.independent
mem_circumsphere_of_two_zsmul_oangle_eq 📖	mathematical	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle EuclideanGeometry.oangle Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere Affine.Simplex.circumsphere	—	Real.instIsStrictOrderedRing Function.update_of_ne Function.update_self affineIndependent_iff_not_collinear_of_ne EuclideanGeometry.collinear_iff_of_two_zsmul_oangle_eq Affine.Simplex.independent circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq Affine.Simplex.mem_circumsphere

EuclideanGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
concyclic_of_two_zsmul_oangle_eq_of_not_collinear 📖	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	Concyclic	—	Real.instIsStrictOrderedRing cospherical_of_two_zsmul_oangle_eq_of_not_collinear coplanar_of_fact_finrank_eq_two
concyclic_or_collinear_of_two_zsmul_oangle_eq 📖	mathematical	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle	Concyclic InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instInsert Set.instSingletonSet Collinear Real.instDivisionRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	Real.instIsStrictOrderedRing cospherical_or_collinear_of_two_zsmul_oangle_eq coplanar_of_fact_finrank_eq_two
cospherical_of_two_zsmul_oangle_eq_of_not_collinear 📖	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	Cospherical	—	Real.instIsStrictOrderedRing collinear_iff_of_two_zsmul_oangle_eq affineIndependent_iff_not_collinear_set cospherical_iff_exists_sphere Affine.Simplex.mem_circumsphere Affine.Triangle.circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq
cospherical_or_collinear_of_two_zsmul_oangle_eq 📖	mathematical	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle	Cospherical Set Set.instInsert Set.instSingletonSet Collinear Real Real.instDivisionRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	Real.instIsStrictOrderedRing Set.insert_eq_self Set.mem_insert_of_mem Set.mem_singleton affineIndependent_iff_not_collinear_set cospherical_iff_exists_sphere Affine.Simplex.mem_circumsphere collinear_iff_of_two_zsmul_oangle_eq Set.insert_comm Collinear.collinear_insert_iff_of_ne Set.mem_insert cospherical_of_two_zsmul_oangle_eq_of_not_collinear

EuclideanGeometry.Cospherical

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
two_zsmul_oangle_eq 📖	mathematical	EuclideanGeometry.Cospherical Set Set.instInsert Set.instSingletonSet	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle EuclideanGeometry.oangle	—	Real.instIsStrictOrderedRing EuclideanGeometry.cospherical_iff_exists_sphere EuclideanGeometry.Sphere.two_zsmul_oangle_eq

EuclideanGeometry.Sphere

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IsTangentAt_iff_angle_eq_pi_div_two 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	IsTangentAt affineSpan Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instInsert Set.instSingletonSet EuclideanGeometry.angle center DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat IsTangentAt.angle_eq_pi_div_two right_mem_affineSpan_pair IsTangentAt_of_angle_eq_pi_div_two
IsTangentAt_of_angle_eq_pi_div_two 📖	mathematical	EuclideanGeometry.angle center Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	IsTangentAt affineSpan Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instInsert Set.instSingletonSet	—	Nat.instAtLeastTwoHAddOfNat left_mem_affineSpan_pair neg_eq_zero inner_neg_right neg_vsub_eq_vsub_rev InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two EuclideanGeometry.angle.eq_1 affineSpan_le
abs_oangle_center_left_toReal_lt_pi_div_two 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	Real Real.instLT abs Real.lattice Real.instAddGroup Real.Angle.toReal EuclideanGeometry.oangle center DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Real.instIsStrictOrderedRing EuclideanGeometry.abs_oangle_right_toReal_lt_pi_div_two_of_dist_eq EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere'
abs_oangle_center_right_toReal_lt_pi_div_two 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	Real Real.instLT abs Real.lattice Real.instAddGroup Real.Angle.toReal EuclideanGeometry.oangle center DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Real.instIsStrictOrderedRing EuclideanGeometry.abs_oangle_left_toReal_lt_pi_div_two_of_dist_eq EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere'
angle_eq_pi_div_two_iff_mem_sphere_ofDiameter 📖	mathematical	—	EuclideanGeometry.angle Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere ofDiameter InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup	—	angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter isDiameter_ofDiameter
angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter 📖	mathematical	IsDiameter InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup	EuclideanGeometry.angle DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	—	Nat.instAtLeastTwoHAddOfNat EuclideanGeometry.mem_sphere' EuclideanGeometry.angle.eq_1 InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two RCLike.charZero_rclike IsDiameter.midpoint_eq_center vsub_add_vsub_cancel inner_add_left inner_add_right left_vsub_midpoint right_vsub_midpoint smul_neg neg_vsub_eq_vsub_rev inner_neg_left real_inner_comm 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg mul_one add_zero neg_add_eq_zero real_inner_self_eq_norm_sq dist_eq_norm_vsub sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing dist_nonneg EuclideanGeometry.mem_sphere IsDiameter.right_mem
dist_div_cos_oangle_center_div_two_eq_radius 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	Real DivInvMonoid.toDiv Real.instDivInvMonoid Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Real.Angle.cos EuclideanGeometry.oangle center instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat radius	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat div_right_comm div_eq_mul_inv mul_comm RCLike.charZero_rclike dist_left_midpoint Real.norm_ofNat EuclideanGeometry.mem_sphere RingHomInvPair.ids tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center EuclideanGeometry.oangle_midpoint_rev_left EuclideanGeometry.oangle.eq_1 vadd_vsub_assoc midpoint_vsub_left invOf_eq_inv smul_inv_smul₀ map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass smul_smul div_mul_cancel₀ two_ne_zero' CharZero.NeZero.two dist_eq_norm_vsub' add_comm Orientation.oangle_add_right_smul_rotation_pi_div_two Real.Angle.cos_coe Real.cos_arctan Nat.cast_one one_div div_inv_eq_mul IsStrictOrderedRing.toPosMulStrictMono IsOrderedRing.toMulPosMono Real.instIsOrderedRing mul_nonneg IsOrderedRing.toPosMulMono norm_nonneg le_of_lt Real.sqrt_pos_of_pos add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE even_two_mul norm_add_sq_eq_norm_sq_add_norm_sq_real Orientation.inner_smul_rotation_pi_div_two_right mul_assoc Real.mul_self_sqrt norm_smul NormedSpace.toNormSMulClass LinearIsometryEquiv.norm_map Real.norm_eq_abs abs_mul_abs_self Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw
dist_div_cos_oangle_center_eq_two_mul_radius 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	Real DivInvMonoid.toDiv Real.instDivInvMonoid Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Real.Angle.cos EuclideanGeometry.oangle center Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat radius	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat dist_div_cos_oangle_center_div_two_eq_radius mul_div_cancel₀ two_ne_zero' CharZero.NeZero.two RCLike.charZero_rclike
dist_div_sin_oangle_div_two_eq_radius 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	Real DivInvMonoid.toDiv Real.instDivInvMonoid Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace abs Real.lattice Real.instAddGroup Real.Angle.sin EuclideanGeometry.oangle instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat radius	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat Real.Angle.abs_cos_eq_abs_sin_of_two_zsmul_add_two_zsmul_eq_pi two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.Angle.cos_nonneg_iff_abs_toReal_le_pi_div_two LT.lt.le abs_oangle_center_right_toReal_lt_pi_div_two dist_div_cos_oangle_center_div_two_eq_radius
dist_div_sin_oangle_eq_two_mul_radius 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	Real DivInvMonoid.toDiv Real.instDivInvMonoid Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace abs Real.lattice Real.instAddGroup Real.Angle.sin EuclideanGeometry.oangle Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat radius	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat dist_div_sin_oangle_div_two_eq_radius mul_div_cancel₀ two_ne_zero' CharZero.NeZero.two RCLike.charZero_rclike
inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	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 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 DivInvMonoid.toDiv Real.instDivInvMonoid Real.instInv Real.Angle.tan EuclideanGeometry.oangle instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike Orientation.rotation EuclideanGeometry.o Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing Real.Angle.coe Real.pi VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup midpoint Real.instRing invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Real.instField RCLike.charZero_rclike NormedAddCommGroup.toAddCommGroup center	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids RCLike.charZero_rclike Real.Angle.tan_eq_inv_of_two_zsmul_add_two_zsmul_eq_pi add_comm two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center
isDiameter_of_angle_eq_pi_div_two 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere EuclideanGeometry.angle Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	IsDiameter InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_zero_add Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_zero 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.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.Linarith.lt_of_eq_of_lt neg_eq_zero 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 EuclideanGeometry.angle_self_of_ne Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.sub_neg_of_lt Real.pi_pos isDiameter_ofDiameter EuclideanGeometry.eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two FiniteDimensional.of_finrank_eq_succ Fact.out IsDiameter.left_mem IsDiameter.right_mem angle_eq_pi_div_two_iff_mem_sphere_ofDiameter
oangle_center_eq_two_zsmul_oangle 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	EuclideanGeometry.oangle center Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing EuclideanGeometry.oangle.eq_1 Orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real dist_eq_norm_vsub EuclideanGeometry.mem_sphere Orientation.oangle.congr_simp vsub_sub_vsub_cancel_right
oangle_eq_pi_sub_two_zsmul_oangle_center_left 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	EuclideanGeometry.oangle center Real.Angle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle Real.Angle.coe Real.pi SubNegMonoid.toZSMul	—	Real.instIsStrictOrderedRing EuclideanGeometry.oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere'
oangle_eq_pi_sub_two_zsmul_oangle_center_right 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	EuclideanGeometry.oangle center Real.Angle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle Real.Angle.coe Real.pi SubNegMonoid.toZSMul	—	Real.instIsStrictOrderedRing oangle_eq_pi_sub_two_zsmul_oangle_center_left EuclideanGeometry.oangle_eq_oangle_of_dist_eq EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere'
tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	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 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 DivInvMonoid.toDiv Real.instDivInvMonoid Real.Angle.tan EuclideanGeometry.oangle center instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike Orientation.rotation EuclideanGeometry.o Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing Real.Angle.coe Real.pi 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 EuclideanGeometry.dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere EuclideanGeometry.oangle_midpoint_rev_left EuclideanGeometry.oangle.eq_1 vadd_vsub_assoc midpoint_vsub_left invOf_eq_inv smul_inv_smul₀ map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass smul_smul add_comm Orientation.tan_oangle_add_right_smul_rotation_pi_div_two mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass two_ne_zero' CharZero.NeZero.two
thales_theorem 📖	mathematical	IsDiameter InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup	EuclideanGeometry.angle DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	—	angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter
two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup EuclideanGeometry.oangle center Real.Angle.coe Real.pi	—	Real.instIsStrictOrderedRing oangle_center_eq_two_zsmul_oangle oangle_eq_pi_sub_two_zsmul_oangle_center_right add_sub_cancel
two_zsmul_oangle_eq 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle EuclideanGeometry.oangle	—	Real.instIsStrictOrderedRing EuclideanGeometry.oangle.eq_1 vsub_sub_vsub_cancel_right Orientation.two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq dist_eq_norm_vsub EuclideanGeometry.mem_sphere Orientation.oangle.congr_simp

EuclideanGeometry.Sphere.IsTangentAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
angle_eq_pi_div_two 📖	mathematical	EuclideanGeometry.Sphere.IsTangentAt AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	EuclideanGeometry.angle EuclideanGeometry.Sphere.center DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	inner_left_eq_zero_of_mem Nat.instAtLeastTwoHAddOfNat EuclideanGeometry.angle.eq_1 neg_vsub_eq_vsub_rev InnerProductGeometry.angle_neg_right InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two 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.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Nat.cast_one Mathlib.Tactic.Ring.one_mul 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.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero 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_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true

Orientation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
oangle_eq_two_zsmul_oangle_sub_of_norm_eq 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm	oangle Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle SubNegMonoid.toSub	—	Real.instIsStrictOrderedRing norm_eq_zero norm_zero norm_ne_zero_iff oangle_sub_left oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.subst_into_smulg Mathlib.Tactic.Abel.term_smulg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.zero_smulg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Abel.zero_termg Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Meta.NormNum.IsInt.neg_to_eq Mathlib.Meta.NormNum.isInt_mul oangle_sub_right sub_ne_zero_of_ne oangle_neg_neg neg_sub
oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm	oangle Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle SubNegMonoid.toSub	—	Real.instIsStrictOrderedRing oangle_eq_two_zsmul_oangle_sub_of_norm_eq
two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle SubNegMonoid.toSub	—	Real.instIsStrictOrderedRing oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real

---

← Back to Index