Theorem star_nnrat_smul

Modification history

2024-10-02 21:25
Mathlib/Algebra/Star/Module.lean
feat: `star` commutes with `nnqsmul` (#17351) …
Added star_nnrat_smulView on Github →