leanprover-community/mathlib

Pull Requests Commits
Remove unnecessary lemma
Smaug123 committed 3 years ago
0b7af667
Close a sorry
Smaug123 committed 3 years ago
8be3898f
Add in the easy proofs for f > 0 and f < 0
Smaug123 committed 3 years ago
1897827c
wip
Smaug123 committed 3 years ago
06e7bd39
Some extra effort
Smaug123 committed 3 years ago
8bb72832
Remove spare hypothesis
Smaug123 committed 3 years ago
cb6e55a1
Tighten bound
Smaug123 committed 3 years ago
c014e164
Add comment
Smaug123 committed 3 years ago
bc1a362b
WIP
Smaug123 committed 3 years ago
ef64300d
Much more progress
Smaug123 committed 3 years ago
a17d424d
WIP
Smaug123 committed 3 years ago
0899f8e9
WIP
Smaug123 committed 3 years ago
eef2ed55
WIP showing convergence if sqrt_aux gets near the answer
Smaug123 committed 3 years ago
0e50527e
Redefine sqrt_aux to have nicer properties
Smaug123 committed 3 years ago
9231e4d7
Lint
Smaug123 committed 3 years ago
a57a9f20
This is looking ominous
Smaug123 committed 3 years ago
430413a3
Replace many proofs with ones that already exist
Smaug123 committed 3 years ago
7d0335ff
Prove that sqrt_aux is positive if f is
Smaug123 committed 3 years ago
c47c7874
Prove that f <= sqrt_aux^2
Smaug123 committed 3 years ago
45918898
feat(computability/partrec_code): add eval prec helpers (#11945)
BoltonBailey committed 3 years ago
82348a60
chore(scripts): update nolints.txt (#13493)
leanprover-community-bot committed 3 years ago
279b7f34
feat(analysis/convex): golf some proofs (#13451)
urkud committed 3 years ago
e6322c6a
feat(data/fin/tuple/nat_antidiagonal): add `list.nat.antidiagonal_tuple_pairwise_pi_lex` (#13339)
eric-wieser committed 3 years ago
b90e770f
chore(algebra/big_operators/fin): moving lemmas (#13331)
joelriou committed 3 years ago
9380977b
feat(topology/[separation, homeomorph]): separation properties are topological invariants (#13401)
ADedecker committed 3 years ago
7c7f3514
feat(topology/algebra/order): extreme value thm for a function continuous on a closed set (#13348)
urkud committed 3 years ago
49e41eb5
chore(scripts): update nolints.txt (#13482)
leanprover-community-bot committed 3 years ago
f4f46cd5
feat(data/finsupp/basic): add a few lemmas, mostly about `finsupp.filter` (#13457)
urkud committed 3 years ago
d4fda045
chore(number_theory/*): Weaken assumptions (#13443)
YaelDillies committed 3 years ago
96667b51
chore(order/bounded_order): Match the `with_bot` and `with_top` API (#13419)
YaelDillies committed 3 years ago
018e9b57
Terms Of Use Privacy Policy Refund Policy Impressum