Theorems · Definition · geometry
Affine.Triangle
(k : Type u_1) →
{V : Type u_2} →
(P : Type u_5) → [inst : Ring k] → [inst_1 : AddCommGroup V] → [Module k V] → [AddTorsor V P] → Type u_5A Triangle k P is a collection of three affinely independent points.
- Cited by
- 75 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- AddCommGroupstatement and proof · cited by 12,871
- Ringstatement and proof · cited by 7,463
- AddTorsorstatement and proof · cited by 1,657
- Affine.Simplexproof · cited by 471
Cited by79
Results whose statement or proof uses this declaration.
- Affine.Triangle.orthocenterstatement and proof · cited by 23
- Affine.Triangle.orthocenter_eq_mongePointstatement and proof · cited by 7
- Affine.Triangle.toPolygonstatement and proof · cited by 4
- EuclideanGeometry.OrthocentricSystemproof · cited by 4
- Affine.Triangle.dist_orthocenter_reflection_circumcenterstatement and proof · cited by 3
- Affine.Triangle.eq_excenter_of_two_zsmul_oangle_eqstatement and proof · cited by 3
- Polygon.toTrianglestatement · cited by 3
- Affine.Triangle.altitude_eq_mongePlanestatement and proof · cited by 2
- Affine.Triangle.circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eqstatement and proof · cited by 2
- Affine.Triangle.dist_div_sin_oangle_div_two_eq_circumradiusstatement and proof · cited by 2
- EuclideanGeometry.exists_dist_eq_circumradius_of_subset_insert_orthocenterstatement and proof · cited by 2
- Affine.Triangle.dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eqstatement and proof · cited by 2