Commit 2025-08-07 03:39 1ab0f168

View on Github →

refactor(LinearAlgebra/AffineSpace/Independent) move simplex to Simplex.Basic and Simplex.Centroid (#27917) This PR is the first step in the migration and split; see discussion in #27881 . This is part of a series; the next PR: #27919

  • Move simplex related material from LinearAlgebra.AffineSpace.Independent to a new Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
  • Move the centroid of simplex related material from LinearAlgebra.AffineSpace.Independent to a new Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
  • No changes or additions to any theorems, definitions, or proofs.
  • Added docstrings for the new files: LinearAlgebra.AffineSpace.Simplex.Basic and LinearAlgebra.AffineSpace.Simplex.Centroid.
  • Modified the docstring in LinearAlgebra.AffineSpace.Independent.
  • Fix the imports in LinearAlgebra.AffineSpace.FiniteDimensional, Geometry.Euclidean.Circumcenter and Analysis.Normed.Affine.Simplex Dependency map: Before: LinearAlgebra.AffineSpace.Independent depends on LinearAlgebra.AffineSpace.Combination After: LinearAlgebra.AffineSpace.Independent depends on LinearAlgebra.AffineSpace.Combination LinearAlgebra.AffineSpace.Simplex.Basic depends on LinearAlgebra.AffineSpace.Independent LinearAlgebra.AffineSpace.Simplex.Centroid depends on LinearAlgebra.AffineSpace.Simplex.Basic

Estimated changes

deleted theorem Affine.Simplex.ext
deleted def Affine.Simplex.face
deleted theorem Affine.Simplex.face_map
deleted def Affine.Simplex.map
deleted theorem Affine.Simplex.map_comp
deleted theorem Affine.Simplex.map_id
deleted structure Affine.Simplex
added theorem Affine.Simplex.ext
added theorem Affine.Simplex.map_id
added structure Affine.Simplex