mathlib3
9db72700 - chore(*): rename gsmul to zsmul and gmultiples to zmultiples (#10010)

Commit

4 years ago

chore(*): rename gsmul to zsmul and gmultiples to zmultiples (#10010) This is consistent with an earlier rename from `gpow` to `zpow`.

Author

sgouezel

Parents