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

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

ericrbg wants to merge 1 commit into master from ericrbg-patch-1
ericrbg
ericrbg chore(modular_forms/basic): fix typo in docs
62a0a3ac
ericrbg ericrbg added easy
ericrbg ericrbg added awaiting-review
ericrbg ericrbg added docs
sgouezel
github-actions github-actions added ready-to-merge
github-actions github-actions removed awaiting-review
bors
bors bors changed the title chore(modular_forms/basic): fix typo in docs [Merged by Bors] - chore(modular_forms/basic): fix typo in docs 2 years ago
bors bors closed this 2 years ago
bors bors deleted the ericrbg-patch-1 branch 2 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
Milestone