A couple of easy PRs

Stream: maths

[Matias Heikkilä]

Hey Mathlib people! I recently decided to try my hand at a couple of tiny PRs, looking forward to your feedback :) See e.g. https://github.com/leanprover-community/mathlib/pull/16388