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

35 Open 56 Closed
35 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

primes_infinite uses Nat.factorial (n + 1) instead of Nat.factorial n
#253 opened Nov 10, 2024 by thielema
The behavior of the "obtain" tactic is different from the description in section 3.2
#251 opened Nov 5, 2024 by ctchou
Subgroup closure
#249 opened Oct 21, 2024 by PatrickMassot
Guidance on Formalizing Probability Theory and Request for Tutorials
#248 opened Oct 19, 2024 by zhimi64
1
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
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.