Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-15 17:58 44010bc6

View on Github →

refactor(linear_algebra/affine_space/combination): bundled affine_combination (#3789) When weighted_vsub_of_point and weighted_vsub became bundled linear_maps on the weights, affine_combination was left as an unbundled function with different argument order from the other two related operations. Make it into a bundled affine_map on the weights, so making it more consistent with the other two operations and allowing general results on affine_maps to be used on affine_combination (as illustrated by the changed proofs of weighted_vsub_vadd_affine_combination and affine_combination_vsub).

Estimated changes