Skip to content

Pull requests: avigad/mathematics_in_lean_source

New pull request New
15 Open 189 Closed
15 Open 189 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Added sphinx copy button extension for copying codeblocks
#389 opened Jan 1, 2026 by pritishkamath Loading…
Remove out-of-area example answer.
#388 opened Dec 29, 2025 by Zoupers Loading…
fix: up-to-date link of managing-type-class-inference in C07S02
#387 opened Dec 22, 2025 by blindFS Loading…
1
Update S02_Algebraic_Structures.lean
#385 opened Dec 16, 2025 by knok16 Loading…
§2.5: explain how to call inf_le_left when arguments are not inferrable
#323 opened Oct 18, 2025 by darijgr Loading…
Minor corrections in Chapters 2--7
#322 opened Oct 18, 2025 by darijgr Loading…
2
add record syntax for defining a value of structure type
#318 opened Sep 8, 2025 by yannickseurin Loading…
Nits c05
#317 opened Sep 5, 2025 by yannickseurin Loading…
Remove note about "cannot find synthesization order for instance"
#316 opened Aug 28, 2025 by eric-wieser Loading…
1
Fix small typo
#307 opened Aug 23, 2025 by fnHoj Loading…
Fix some typos from a brief overview
#303 opened Jul 1, 2025 by pevogam Loading…
1
Nits in Chapter 06 "Discrete Mathematics"
#301 opened Jun 17, 2025 by yannickseurin Loading…
Fix typo
#299 opened May 24, 2025 by nimarasekh Loading…
Add missing theorems and solutions to C02 S01
#279 opened Feb 1, 2025 by gaearon Loading…
2
Add MIL.Common import to intro example
#278 opened Feb 1, 2025 by gaearon Loading…
ProTip! Add no:assignee to see everything that’s not assigned.