Skip to content

Issues: avigad/mathematics_in_lean_source

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

32 Open 56 Closed
32 Open 56 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
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Guidance on Formalizing Probability Theory and Request for Tutorials
#248 opened Oct 19, 2024 by zhimi64
Congruence
#237 opened Sep 9, 2024 by PatrickMassot
Error in backtick parsing with text after closing backticks
#233 opened Aug 29, 2024 by adomasbaliuka
Explaining subtype
#227 opened Aug 19, 2024 by PatrickMassot
Explanation about Inverse function in Chapter 4
#213 opened Jul 12, 2024 by yannickseurin
Explain convert ... using in C03S06
#208 opened Jun 10, 2024 by yannickseurin
Section 2.2: Definition of substraction in a general ring
#202 opened May 24, 2024 by yannickseurin
2
C04/S02: Possible redundant exercise
#199 opened May 3, 2024 by mtoohey31
Replace induction' with induction
#195 opened May 2, 2024 by PatrickMassot
Simp and let
#194 opened May 2, 2024 by PatrickMassot
refine'
#187 opened Apr 18, 2024 by Vilin97
tauto!
#186 opened Apr 18, 2024 by Vilin97
Consider adding the failed example relevant to the bad diamond issue in Chapter7 §1
#185 opened Mar 25, 2024 by onriv
FunLike update
#179 opened Feb 5, 2024 by PatrickMassot
Add a description of apply_fun
#160 opened Dec 17, 2023 by avigad
Missing mentioned function and unused hypothesis
#151 opened Nov 7, 2023 by DiegoBravo
Explain how to define a sequence by recursion inside a proof.
#150 opened Nov 6, 2023 by PatrickMassot
Explain that Pi notation has disappeared
#149 opened Oct 30, 2023 by faenuccio
Groups and rings tweaks
#144 opened Oct 24, 2023 by PatrickMassot
|a * b| ≤ (a ^ 2 + b ^ 2) / 2 exercise uses constructor before it is introduced
#138 opened Oct 20, 2023 by kmill
1
Remove extra parentheses
#133 opened Oct 2, 2023 by PatrickMassot
2
factorial simp example
#132 opened Oct 2, 2023 by PatrickMassot
1
Explain structural eta reduction
#124 opened Sep 4, 2023 by avigad
Set autoimplicit flag to false
#115 opened Aug 26, 2023 by avigad
Topology chapter should teach/warn about products of metric spaces
#93 opened Jul 10, 2023 by fpvandoorn
ProTip! What’s not been updated in a month: updated:<2024-09-20.