Theorems · Theorem · geometry

Affine.Simplex.centroid_eq_iff

∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [CharZero k] {n : ℕ} (s : Affine.Simplex k P n) {fs₁ fs₂ : Finset (Fin (n + 1))} {m₁ m₂ : ℕ},
  fs₁.card = m₁ + 1 → fs₂.card = m₂ + 1 → (Finset.centroid k fs₁ s.points = Finset.centroid k fs₂ s.points ↔ fs₁ = fs₂)

Over a characteristic-zero division ring, the centroids given by two subsets of the points of a simplex are equal if and only if those faces are given by the same subset of points.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Cited by

1 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionRingAddCommGroupModuleAddTorsorCharZero