Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-30 18:34 b18eedb0

View on Github →

feat(linear_algebra/affine_space/combination): add lemma finset.map_affine_combination (#9453) The other included lemmas affine_map.coe_sub, affine_map.coe_neg are unrelated but are included to reduce PR overhead.

Estimated changes