Commit 2025-05-24 22:06 5434c49e

View on Github →

feat: add Affine.Simplex.map and lemmas (#25156)

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

added theorem Affine.Simplex.faceOpposite_map

added theorem Affine.Simplex.face_map

added def Affine.Simplex.map

added theorem Affine.Simplex.map_comp

added theorem Affine.Simplex.map_id

added theorem Affine.Simplex.map_mkOfPoint

added theorem Affine.Simplex.reindex_map