Commit 2024-10-02 21:25 20a854cd

View on Github →

feat: star commutes with nnqsmul (#17351) From LeanAPAP

Estimated changes

Modified Mathlib/Algebra/Star/Module.lean

added theorem star_nnrat_smul

modified theorem star_rat_smul

Modified Mathlib/Data/Matrix/Basic.lean