Documentation Verification Report

NinePointCircle

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

Statistics

Metric	Count
Definitions `eulerPoint`, `ninePointCircle`	2
Theorems `eulerPoint_map`, `eulerPoint_mem_ninePointCircle`, `eulerPoint_reindex`, `eulerPoint_restrict`, `faceOppositeCentroid_mem_ninePointCircle`, `isDiameter_ninePointCircle`, `midpoint_faceOppositeCentroid_eulerPoint`, `ninePointCircle_center`, `ninePointCircle_center_mem_affineSpan`, `ninePointCircle_eq_circumsphere_medial`, `ninePointCircle_map`, `ninePointCircle_radius`, `ninePointCircle_reindex`, `ninePointCircle_restrict`, `orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle`, `points_vsub_eulerPoint`, `altitudeFoot_mem_ninePointCircle`, `eulerPoint_eq_midpoint`	18
Total	20

Affine.Simplex

Definitions

Name	Category	Theorems
`eulerPoint` 📖	CompOp	9 math math: `eulerPoint_mem_ninePointCircle`, `Affine.Triangle.eulerPoint_eq_midpoint`, `midpoint_faceOppositeCentroid_eulerPoint`, `eulerPoint_reindex`, `eulerPoint_restrict`, `eulerPoint_map`, `isDiameter_ninePointCircle`, `orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle`, `points_vsub_eulerPoint`
`ninePointCircle` 📖	CompOp	13 math math: `ninePointCircle_eq_circumsphere_medial`, `ninePointCircle_radius`, `ninePointCircle_restrict`, `Affine.Triangle.altitudeFoot_mem_ninePointCircle`, `eulerPoint_mem_ninePointCircle`, `ninePointCircle_reindex`, `ninePointCircle_center_mem_affineSpan`, `midpoint_faceOppositeCentroid_eulerPoint`, `faceOppositeCentroid_mem_ninePointCircle`, `isDiameter_ninePointCircle`, `orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle`, `ninePointCircle_map`, `ninePointCircle_center`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eulerPoint_map` 📖	mathematical	—	`eulerPoint` `map` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `AffineIsometry.toAffineMap` `AffineIsometry.injective` `DFunLike.coe` `AffineIsometry` `AffineIsometry.instFunLike`	—	`AffineIsometry.injective` `AffineIsometry.coe_toAffineMap` `mongePoint_map` `AffineIsometry.map_vadd` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `LinearIsometry.instSemilinearIsometryClass` `AffineIsometry.map_vsub`
`eulerPoint_mem_ninePointCircle` 📖	mathematical	—	`EuclideanGeometry.Sphere` `EuclideanGeometry.instMembershipSphere` `ninePointCircle` `eulerPoint`	—	`EuclideanGeometry.Sphere.IsDiameter.right_mem` `isDiameter_ninePointCircle`
`eulerPoint_reindex` 📖	mathematical	—	`eulerPoint` `reindex` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`Fin.equiv_iff_eq` `mongePoint_reindex`
`eulerPoint_restrict` 📖	mathematical	`AffineSubspace` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `Preorder.toLE` `PartialOrder.toPreorder` `AffineSubspace.instPartialOrder` `affineSpan` `Set.range` `points`	`SetLike.instMembership` `AffineSubspace.instSetLike` `eulerPoint` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.setLike` `AffineSubspace.direction` `Submodule.normedAddCommGroup` `Submodule.innerProductSpace` `Subtype.metricSpace` `AffineSubspace.toNormedAddTorsor` `Nonempty.map` `DFunLike.coe` `AffineMap` `Submodule.addCommGroup` `Submodule.module` `AffineSubspace.toAddTorsor` `instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `Set.instNonemptyRange` `Set.Elem` `SetLike.coe` `Set.inclusion` `AffineMap.instFunLike` `AffineSubspace.inclusion` `restrict`	—	`Nonempty.map` `instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `Set.instNonemptyRange` `mongePoint_restrict`
`faceOppositeCentroid_mem_ninePointCircle` 📖	mathematical	—	`EuclideanGeometry.Sphere` `EuclideanGeometry.instMembershipSphere` `ninePointCircle` `faceOppositeCentroid` `Real` `Real.instDivisionRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace`	—	`EuclideanGeometry.mem_sphere` `ninePointCircle_center` `ninePointCircle_radius` `dist_circumcenter_eq_circumradius'` `dist_eq_norm_vsub` `eq_div_iff_mul_eq` `RCLike.charZero_rclike` `mul_comm` `RCLike.norm_natCast` `norm_smul` `NormedSpace.toNormSMulClass` `vsub_vadd_eq_vsub_sub` `smul_sub` `smul_smul` `mul_div_cancel₀` `add_smul` `one_smul` `sub_sub` `vsub_sub_vsub_cancel_right` `centroid_vsub_point_eq_smul_vsub` `vsub_sub_vsub_cancel_left`
`isDiameter_ninePointCircle` 📖	mathematical	—	`EuclideanGeometry.Sphere.IsDiameter` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `ninePointCircle` `faceOppositeCentroid` `Real.instDivisionRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `eulerPoint`	—	`faceOppositeCentroid_mem_ninePointCircle` `midpoint_faceOppositeCentroid_eulerPoint`
`midpoint_faceOppositeCentroid_eulerPoint` 📖	mathematical	—	`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` `faceOppositeCentroid` `Real.instDivisionRing` `eulerPoint` `EuclideanGeometry.Sphere.center` `ninePointCircle`	—	`vsub_left_cancel` `RCLike.charZero_rclike` `ninePointCircle_center` `Nat.instAtLeastTwoHAddOfNat` `midpoint_vsub` `vadd_vsub` `eulerPoint.eq_1` `mongePoint_eq_smul_vsub_vadd_circumcenter` `centroid.eq_1` `faceOppositeCentroid_vsub_centroid_eq_smul_vsub` `smul_add` `smul_eq_zero_of_right` `Nat.cast_one` `inv_one` `one_smul` `vsub_add_vsub_cancel` `vsub_self` `invOf_eq_inv` `circumcenter_eq_centroid` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `CharP.cast_eq_zero` `CharP.ofCharZero` `div_zero` `smul_zero` `zero_vadd` `vsub_vadd` `div_one` `Mathlib.Tactic.Zify.Nat.cast_sub_of_lt` `vadd_vadd` `vsub_vadd_eq_vsub_sub` `smul_sub` `sub_add` `smul_smul` `sub_smul` `sub_one_mul` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `lt_trans` `Mathlib.Meta.Positivity.pos_of_isNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `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.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `neg_div` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `mul_neg` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `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.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `neg_mul` `div_mul_div_cancel₀'` `neg_smul` `sub_neg_eq_add` `faceOppositeCentroid_eq_smul_vsub_vadd_point` `vadd_vsub_assoc` `add_add_add_comm` `add_assoc` `Nat.cast_add` `add_comm` `add_div` `div_self` `add_smul` `one_div` `two_smul` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `IsUnit.div_mul_cancel` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_eq_false` `Nat.cast_zero`
`ninePointCircle_center` 📖	mathematical	—	`EuclideanGeometry.Sphere.center` `ninePointCircle` `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.instAdd` `Real.instNatCast` `Real.instOne` `VSub.vsub` `AddTorsor.toVSub` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `centroid` `Real.instDivisionRing` `NormedAddCommGroup.toAddCommGroup` `circumcenter`	—	—
`ninePointCircle_center_mem_affineSpan` 📖	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.range` `points` `EuclideanGeometry.Sphere.center` `ninePointCircle`	—	`ninePointCircle_center` `AffineSubspace.vadd_mem_of_mem_direction` `Submodule.smul_mem` `AffineSubspace.vsub_mem_direction` `centroid_mem_affineSpan` `RCLike.charZero_rclike` `circumcenter_mem_affineSpan`
`ninePointCircle_eq_circumsphere_medial` 📖	mathematical	—	`ninePointCircle` `circumsphere` `medial` `Real` `Real.instDivisionRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `RCLike.charZero_rclike`	—	`RCLike.charZero_rclike` `circumsphere_unique_dist_eq` `affineSpan_range_medial` `ninePointCircle_center_mem_affineSpan` `Set.range_subset_iff` `faceOppositeCentroid_mem_ninePointCircle`
`ninePointCircle_map` 📖	mathematical	—	`ninePointCircle` `map` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `AffineIsometry.toAffineMap` `AffineIsometry.injective` `DFunLike.coe` `AffineIsometry` `AffineIsometry.instFunLike` `EuclideanGeometry.Sphere.center` `EuclideanGeometry.Sphere.radius`	—	`EuclideanGeometry.Sphere.ext` `AffineIsometry.injective` `centroid_map` `RCLike.charZero_rclike` `AffineIsometry.coe_toAffineMap` `circumcenter_map` `AffineIsometry.map_vadd` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `LinearIsometry.instSemilinearIsometryClass` `AffineIsometry.map_vsub` `circumradius_map`
`ninePointCircle_radius` 📖	mathematical	—	`EuclideanGeometry.Sphere.radius` `ninePointCircle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `circumradius` `Real.instNatCast`	—	—
`ninePointCircle_reindex` 📖	mathematical	—	`ninePointCircle` `reindex` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace`	—	`Fin.equiv_iff_eq` `EuclideanGeometry.Sphere.ext` `centroid_reindex` `circumcenter_reindex` `circumradius_reindex`
`ninePointCircle_restrict` 📖	mathematical	`AffineSubspace` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `Preorder.toLE` `PartialOrder.toPreorder` `AffineSubspace.instPartialOrder` `affineSpan` `Set.range` `points`	`ninePointCircle` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `AffineSubspace.direction` `AffineSubspace.instSetLike` `Submodule.normedAddCommGroup` `Submodule.innerProductSpace` `Subtype.metricSpace` `AffineSubspace.toNormedAddTorsor` `Nonempty.map` `DFunLike.coe` `AffineMap` `Submodule.addCommGroup` `Submodule.module` `AffineSubspace.toAddTorsor` `instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `Set.instNonemptyRange` `Set.Elem` `SetLike.coe` `Set.inclusion` `AffineMap.instFunLike` `AffineSubspace.inclusion` `restrict` `EuclideanGeometry.Sphere.center` `Set.mem_of_mem_of_subset` `ninePointCircle_center_mem_affineSpan` `EuclideanGeometry.Sphere.radius`	—	`EuclideanGeometry.Sphere.ext` `Nonempty.map` `instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `Set.instNonemptyRange` `Set.mem_of_mem_of_subset` `ninePointCircle_center_mem_affineSpan` `centroid_restrict` `RCLike.charZero_rclike` `circumcenter_restrict` `circumradius_restrict`
`orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle` 📖	mathematical	—	`EuclideanGeometry.Sphere` `EuclideanGeometry.instMembershipSphere` `ninePointCircle` `AffineSubspace` `Real` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Real.instRCLike` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set.range` `points` `faceOpposite` `Real.instRing` `Real.normedField` `DFunLike.coe` `ContinuousAffineMap` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.setLike` `AffineSubspace.direction` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Submodule.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Submodule.module` `instTopologicalSpaceSubtype` `AffineSubspace.toAddTorsor` `instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `Set.instNonemptyRange` `ContinuousAffineMap.instFunLike` `orthogonalProjectionSpan` `eulerPoint`	—	`instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `Set.instNonemptyRange` `Nat.instAtLeastTwoHAddOfNat` `EuclideanGeometry.Sphere.thales_theorem` `isDiameter_ninePointCircle` `orthogonalProjectionSpan.eq_1` `EuclideanGeometry.angle_orthogonalProjection_self` `Submodule.HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `FiniteDimensional.RCLike.properSpace_submodule` `finiteDimensional_direction_affineSpan_range` `Finite.of_fintype` `faceOppositeCentroid_mem_affineSpan_face` `RCLike.charZero_rclike`
`points_vsub_eulerPoint` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `points` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `eulerPoint` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instSub` `Real.instNatCast` `Real.instOne` `mongePoint`	—	`eulerPoint.eq_1` `vsub_vadd_eq_vsub_sub` `Subsingleton.eq_zero` `AffineSubspace.mem_affineSpan_singleton` `mongePoint_mem_affineSpan` `vsub_self` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `inv_zero` `smul_zero` `sub_self` `zero_sub` `div_zero` `sub_div` `div_self` `one_div` `sub_smul` `one_smul`

Affine.Triangle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`altitudeFoot_mem_ninePointCircle` 📖	mathematical	—	`EuclideanGeometry.Sphere` `EuclideanGeometry.instMembershipSphere` `Affine.Simplex.ninePointCircle` `Affine.Simplex.altitudeFoot`	—	`instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `Set.instNonemptyRange` `Affine.Simplex.altitudeFoot.eq_1` `EuclideanGeometry.orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem` `Affine.Simplex.points_vsub_eulerPoint` `Submodule.smul_mem_iff` `IsScalarTower.left` `Mathlib.Meta.NormNum.isNNRat_eq_false` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_sub` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Nat.cast_zero` `orthocenter_eq_mongePoint` `direction_affineSpan` `Affine.Simplex.range_faceOpposite_points` `Set.mem_of_mem_of_subset` `AffineSubspace.vsub_mem_direction` `Affine.Simplex.mem_altitude` `orthocenter_mem_altitude` `Submodule.IsOrtho.ge` `Affine.Simplex.vectorSpan_isOrtho_altitude_direction` `Affine.Simplex.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle`
`eulerPoint_eq_midpoint` 📖	mathematical	—	`Affine.Simplex.eulerPoint` `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` `orthocenter` `Affine.Simplex.points`	—	`vsub_right_cancel` `RCLike.charZero_rclike` `orthocenter_eq_mongePoint` `Affine.Simplex.points_vsub_eulerPoint` `Nat.instAtLeastTwoHAddOfNat` `vsub_midpoint` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_sub` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `invOf_eq_inv` `vsub_self` `smul_zero` `add_zero`

---

← Back to Index