Commit 2024-07-22 23:57 de6c2cd2

View on Github →

chore: rename Basis.smul to Basis.smulTower (#15036) This makes room for a SMul instance and lemmas about it Moves:

  • Basis.smul -> Basis.smulTower
  • Basis.smul_repr -> Basis.smulTower_repr
  • Basis.smul_repr_mk -> Basis.smulTower_repr_mk
  • Basis.smul_apply -> Basis.smulTower_apply
  • Basis.smul_leftMulMatrix -> Basis.smulTower_leftMulMatrix
  • Basis.smul_leftMulMatrix_algebraMap -> Basis.smulTower_leftMulMatrix_algebraMap
  • Basis.smul_leftMulMatrix_algebraMap_eq -> Basis.smulTower_leftMulMatrix_algebraMap_eq
  • Basis.smul_leftMulMatrix_algebraMap_ne -> Basis.smulTower_leftMulMatrix_algebraMap_ne Zulip thread

Estimated changes

added theorem Basis.smulTower_apply
added theorem Basis.smulTower_repr
deleted theorem Basis.smul_apply
deleted theorem Basis.smul_repr
deleted theorem Basis.smul_repr_mk