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

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

Review dot notation explanations
#268 opened Dec 9, 2024 by PatrickMassot
DenseInducing.continuousAt_extend does not seem to exist
#267 opened Dec 9, 2024 by ctchou
MIL/C10_Topology/solutions/Solutions_S02_Metric_Spaces.lean is not complete
#266 opened Dec 6, 2024 by ctchou
Minor issue in sec.10.2.1
#265 opened Dec 1, 2024 by ctchou
MIL/C09_Linear_Algebra/solutions/Solutions_S0{2,3,4}_*.lean do not compile
#262 opened Nov 25, 2024 by ctchou
The example involving quotient in sec.7.3 needs more detailed explanations
#261 opened Nov 22, 2024 by ctchou
Every finite set of natural numbers cannot contain all prime numbers
#260 opened Nov 22, 2024 by thielema
Simpler variant of Cantor's diagonal argument
#259 opened Nov 22, 2024 by thielema
Last example of sec.8.2.3 is not consistent with the text describing it
#258 opened Nov 22, 2024 by ctchou
Redundant arguments
#257 opened Nov 21, 2024 by ctchou
dot notation with coercions
#256 opened Nov 18, 2024 by fpvandoorn
Instance names seem unnecessary after all
#255 opened Nov 13, 2024 by ctchou
There is no GroupCat in Mathlib
#254 opened Nov 13, 2024 by ctchou
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
ProTip! Add no:assignee to see everything that’s not assigned.