Documentation Verification Report

Simplex

📁 Source: Mathlib/Geometry/Euclidean/Simplex.lean

Statistics

Metric	Count
Definitions `AcuteAngled`	1
Theorems `acuteAngled`, `angle_eq_pi_div_three`, `acuteAngled_reindex_iff`, `dist_point_centroid`, `dist_point_faceOppositeCentroid`, `acuteAngled_iff_angle_lt`, `dist_point_centroid`, `dist_point_faceOppositeCentroid`	8
Total	9

Affine.Simplex

Definitions

Name	Category	Theorems
`AcuteAngled` 📖	MathDef	3 math math: `Equilateral.acuteAngled`, `Affine.Triangle.acuteAngled_iff_angle_lt`, `acuteAngled_reindex_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`acuteAngled_reindex_iff` 📖	mathematical	—	`AcuteAngled` `reindex` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace`	—	`Equiv.symm_apply_apply` `EquivLike.toEmbeddingLike`
`dist_point_centroid` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `points` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `centroid` `Real.instDivisionRing` `Real.instMul` `Real.instNatCast` `faceOppositeCentroid`	—	`dist_eq_norm_vsub` `point_vsub_centroid_eq_smul_vsub` `RCLike.charZero_rclike` `norm_smul` `NormedSpace.toNormSMulClass` `Real.norm_natCast`
`dist_point_faceOppositeCentroid` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `points` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `faceOppositeCentroid` `Real.instDivisionRing` `Real.instMul` `Real.instAdd` `Real.instNatCast` `Real.instOne` `centroid`	—	`dist_eq_norm_vsub` `point_vsub_faceOppositeCentroid_eq_smul_vsub` `RCLike.charZero_rclike` `norm_smul` `NormedSpace.toNormSMulClass` `Nat.cast_one` `RCLike.norm_natCast`

Affine.Simplex.Equilateral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`acuteAngled` 📖	mathematical	`Affine.Simplex.Equilateral` `Real` `Real.instRing` `NormedAddCommGroup.toSeminormedAddCommGroup` `MetricSpace.toPseudoMetricSpace` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike`	`Affine.Simplex.AcuteAngled`	—	`Nat.instAtLeastTwoHAddOfNat` `angle_eq_pi_div_three` `lt_of_not_ge` `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` `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` `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.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Real.instIsStrictOrderedRing` `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` `Nat.cast_one` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_nonpos` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Meta.NormNum.isNat_lt_true` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.pi_pos`
`angle_eq_pi_div_three` 📖	mathematical	`Affine.Simplex.Equilateral` `Real` `Real.instRing` `NormedAddCommGroup.toSeminormedAddCommGroup` `MetricSpace.toPseudoMetricSpace` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike`	`EuclideanGeometry.angle` `Affine.Simplex.points` `NormedAddCommGroup.toAddCommGroup` `NormedAddTorsor.toAddTorsor` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `EuclideanGeometry.angle.eq_1` `InnerProductGeometry.angle.eq_1` `real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two` `Real.arccos_eq_of_eq_cos` `le_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.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_zero` `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.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.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `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` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_lt_true` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.pi_nonneg` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Linarith.mul_nonpos` `vsub_sub_vsub_cancel_right` `Real.cos_pi_div_three` `AffineIndependent.injective` `Real.instNontrivial` `Affine.Simplex.independent` `dist_eq_zero` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `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.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `Mathlib.Meta.NormNum.isNat_eq_false` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Meta.NormNum.isNat_add`

Affine.Triangle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`acuteAngled_iff_angle_lt` 📖	mathematical	—	`Affine.Simplex.AcuteAngled` `Real` `Real.instLT` `EuclideanGeometry.angle` `Affine.Simplex.points` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `EuclideanGeometry.angle_comm` `Fintype.complete`
`dist_point_centroid` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Affine.Simplex.points` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `Affine.Simplex.centroid` `Real.instDivisionRing` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Affine.Simplex.faceOppositeCentroid`	—	`Nat.instAtLeastTwoHAddOfNat` `Affine.Simplex.dist_point_centroid`
`dist_point_faceOppositeCentroid` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Affine.Simplex.points` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `Affine.Simplex.faceOppositeCentroid` `Real.instDivisionRing` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Affine.Simplex.centroid`	—	`Nat.instAtLeastTwoHAddOfNat` `Affine.Simplex.dist_point_faceOppositeCentroid` `Nat.cast_one`

---

← Back to Index