|
|
ad20702327
|
BadInfinities: chore redundant newline
|
2025-04-08 23:05:57 -04:00 |
|
|
|
b744e862f4
|
BadInfinities: fix no_int_infinity
|
2025-04-08 22:43:43 -04:00 |
|
|
|
59d9058103
|
BadInfinities
|
2025-04-08 22:31:48 -04:00 |
|
|
|
e6d72e3b82
|
not_f_eq_imp_eq
|
2025-04-08 22:19:21 -04:00 |
|
|
|
d914baf772
|
all: use standard theorem identifier scheme
https://leanprover-community.github.io/contribute/naming.html
|
2025-04-08 22:13:50 -04:00 |
|
|
|
3f9948eaf9
|
FinitudeOfPropositions
|
2025-04-08 22:10:20 -04:00 |
|
|
|
43b0af409b
|
RunMEvil: simplify proofs
|
2025-04-08 21:57:48 -04:00 |
|
|
|
38c00b3311
|
lawfulRunMEvil
|
2025-04-08 21:54:27 -04:00 |
|
|
|
2573d64897
|
runMEvil
|
2025-04-08 21:49:57 -04:00 |
|
