mathlib3

[Merged by Bors] - chore(modular_forms/basic): fix typo in docs

#19166

Closed