Affine.Simplex.sum_pointsWithCircumcenter
∀ {α : Type u_3} [inst : AddCommMonoid α] {n : ℕ} (f : Affine.Simplex.PointsWithCircumcenterIndex n → α),
∑ i, f i =
∑ i, f (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex i) +
f Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndexThe sum of a function over PointsWithCircumcenterIndex.
- Defined in
- Mathlib.Geometry.Euclidean.Circumcenter
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Finsetproof · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- Finset.sumstatement and proof · cited by 5,195
- Finset.univstatement and proof · cited by 3,473
- add_commproof · cited by 1,535
- Finset.mapproof · cited by 747
- Finset.extproof · cited by 565
- Finset.mem_univproof · cited by 361
- Finset.sum_insertproof · cited by 196
- Finset.mem_insert_selfproof · cited by 128
- Finset.sum_mapproof · cited by 115
Cited by7
Results whose statement or proof uses this declaration.
- Affine.Triangle.dist_orthocenter_reflection_circumcenterproof · cited by 3
- Affine.Simplex.centroid_eq_affineCombination_of_pointsWithCircumcenterproof · cited by 3
- Affine.Simplex.sum_mongePointWeightsWithCircumcenterproof · cited by 2
- Affine.Simplex.sum_reflectionCircumcenterWeightsWithCircumcenterproof · cited by 1
- Affine.Simplex.sum_centroidWeightsWithCircumcenterproof · cited by 1
- Affine.Simplex.inner_mongePoint_vsub_face_centroid_vsubproof · cited by 1