Ptolemy

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

Statistics

Metric	Count
Definitions	0
Theorems mul_dist_add_mul_dist_eq_mul_dist_of_cospherical	1
Total	1

EuclideanGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_dist_add_mul_dist_eq_mul_dist_of_cospherical 📖	mathematical	Cospherical Set Set.instInsert Set.instSingletonSet angle Real.pi	Real Real.instAdd Real.instMul Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace	—	Set.insert_comm mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi left_dist_ne_zero_of_angle_eq_pi dist_mul_of_eq_angle_of_dist_mul angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi angle_comm mul_comm Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero dist_comm Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ mul_left_comm dist_eq_add_dist_of_angle_eq_pi Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval dist_sq_mul_dist_add_dist_sq_mul_dist IsDomain.toIsCancelMulZero Real.instIsDomain AddLeftCancelSemigroup.toIsLeftCancelAdd

---

← Back to Index