mathlib3

59150e4a - chore(modular_forms/basic): fix typo in docs (#19166)