Commit 2025-03-31 10:57 ccac78f1

View on Github →

feat(LinearAlgebra/AffineSpace/Independent): faceOpposite (#22745) Add a convenience definition for the face of a simplex opposite a given vertex (the face with all but that one vertex of the original simplex).

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

added def Affine.Simplex.faceOpposite

added theorem Affine.Simplex.mem_affineSpan_range_faceOpposite_points_iff

added theorem Affine.Simplex.mem_affineSpan_range_face_points_iff

added theorem Affine.Simplex.range_faceOpposite_points