leanprover-community/mathlib

Pull Requests Commits
Attempt at fixing breakage
vihdzp committed 4 years ago
315e26f7
Merge branch 'unbounded' into deriv_fp_enum
vihdzp committed 4 years ago
7e473c11
Minor tweaks
vihdzp committed 4 years ago
65bc29f5
Pretty much redid the whole unbounded thing
vihdzp committed 4 years ago
9f356682
Merge branch 'unbounded' into deriv_fp_enum
vihdzp committed 4 years ago
e81cd47f
Proved corresponding `ge` cases
vihdzp committed 4 years ago
7fdd5731
Used typeclass
vihdzp committed 4 years ago
1263fddc
Lots of rewriting
vihdzp committed 4 years ago
5e6fc9bd
feat(normed_space/lp_space): Lp space for `Π i, E i` (#11015)
hrmacbeth committed 4 years ago
1594b0ca
Got some unbreaking to do
vihdzp committed 4 years ago
ae8284e8
Merge branch 'unbounded' into deriv_fp_enum
vihdzp committed 4 years ago
e8dcf742
Tiny tweaks
vihdzp committed 4 years ago
948bb31b
Fixed theorem name
vihdzp committed 4 years ago
b82aafe6
Added a bunch of extra results
vihdzp committed 4 years ago
5d7f38da
Proved `unbounded_iff`
vihdzp committed 4 years ago
7eee2dd7
Merge branch 'lub_new' into enum_ord
vihdzp committed 4 years ago
b9c047af
Merge branch 'master' into enum_ord
vihdzp committed 4 years ago
9d23f22d
Merge branch 'lub_new' into lub_new'
vihdzp committed 4 years ago
f4bd3868
Merge branch 'master' into lub_new
vihdzp committed 4 years ago
12d49dda
Merge branch 'lub_new'' into fp_enum_simple
vihdzp committed 4 years ago
afa69403
feat(data/set/*): lemmas about `monotone`/`antitone` and sets/intervals (#11173)
urkud committed 4 years ago
742ec88c
fix(order/filter/ultrafilter): dedup instance names (#11171)
kbuzzard committed 4 years ago
979f2e72
feat(combinatorics/simple_graph/srg): is_SRG_with for complete graphs, edgeless graphs, and complements (#5698)
agusakov committed 4 years ago
da54388a
Very small golf
vihdzp committed 4 years ago
a5430206
Proved extra stuff
vihdzp committed 4 years ago
6b749890
Merge branch 'deriv_fp_enum' into fp_enum_simple
vihdzp committed 4 years ago
81f132ac
Small golf
vihdzp committed 4 years ago
85706a87
Merge branch 'enum_ord' into deriv_fp_enum
vihdzp committed 4 years ago
fbb11326
Extra golfing
vihdzp committed 4 years ago
7cb1f453
Removed redundant `noncomputable`
vihdzp committed 4 years ago
8246343f
Terms Of Use Privacy Policy Refund Policy Impressum