Commit 2025-08-15 22:00 595c2c61

View on Github →

refactor: tidy mulVec and vecMul lemmas about • (#28450) This deprecates two _assoc lemmas, and moves a third without deprecation to resolve a name clash. Only mulVec_smul was previously correctly-named (but duplicated). vecMul_smul was missing altogether. Moves:

  • Matrix.smul_mulVec_assoc -> Matrix.smul_mulVec
  • Matrix.mulVec_smul_assoc -> Matrix.mulVec_smul
  • Matrix.vecMul_smul -> Matrix.smul_vecMul

Estimated changes

modified theorem Matrix.mulVec_smul
added theorem Matrix.smul_mulVec
deleted theorem Matrix.smul_mulVec_assoc
added theorem Matrix.smul_vecMul
modified theorem Matrix.vecMul_smul