mathlib3

2de9c37f - chore(linear_algebra/affine_space/combination): make k explicit in affine_combination (#18689)

chore(linear_algebra/affine_space/combination): make k explicit in affine_combination (#18689) The implicitness caused problems in elaboration. In Lean 3 it only amounts to long elaboration times, but in Lean 4 elaboration fails.