Commit 2024-11-26 17:39 19094c4d

feat: handle scalar multiplication in linear_combination (#19136) This PR extends linear_combination to handle scalar multiplication. Examples (under sensible typeclasses, here omitted):

example {a b : K} {x : V} (h : a ^ 2 + b ^ 2 = 1) :
    a • (a • x - b • y) + (b • a • y + b • b • x) = x := by
  linear_combination (norm := module) h • x
example {v w x y : V} (h₁ : x - y = -(v - w)) (h₂ : x + y = v + w) : x = w := by
  linear_combination (norm := module) (2:K)⁻¹ • (h₁ + h₂)
example {a b : K} {x y z : V} (hb : 0 ≤ b) (hab : a + b = 1) (H : z ≤ a • x + b • y) (hyz : y ≤ z) :
    a • z ≤ a • x := by
  linear_combination (norm := skip) b • hyz + hab • z + H
  apply le_of_eq
  module

As is apparent from these examples, it is still generally necessary to invoke a nonstandard discharger (generally module or match_scalars) when using linear_combination with this new feature, since the default discharger (ring) is not usually useful on module goals.