Skip to content
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

Jump to bottom

[Merged by Bors] - refactor(analysis/analytic/basic): refactor change_origin #8282

Closed
wants to merge 34 commits into from
Closed

[Merged by Bors] - refactor(analysis/analytic/basic): refactor change_origin #8282

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
34 commits
Select commit Hold shift + click to select a range
6b91db1
Snapshot
urkud Feb 19, 2021
322e7d4
Merge branch 'master' into change-origin
urkud Feb 25, 2021
5f33328
Snapshot
urkud Feb 25, 2021
8a9643d
Snapshot
urkud Feb 27, 2021
b18a715
Merge branch 'master' into change-origin
urkud Apr 4, 2021
4fb38f1
chore(data/real/nnreal): use `function.injective.*` constructors
urkud Apr 4, 2021
2f4dee3
Fix compile
urkud Apr 4, 2021
f899c2f
Merge commit '4fb38f122' into change-origin
urkud Apr 4, 2021
b3e5eab
Merge branch 'nnreal-instance' into change-origin
urkud Apr 4, 2021
cf32258
Snapshot
urkud Apr 6, 2021
2738fff
Snapshot
urkud Apr 6, 2021
e7b995c
Snapshot
urkud Apr 8, 2021
96f9d69
Merge branch 'master' into change-origin
urkud Apr 11, 2021
1376ca1
Merge branch 'master' into change-origin
urkud Jun 21, 2021
e21d263
Merge branch 'master' into change-origin
urkud Jul 10, 2021
38cb0c7
Remove some unneeded inequalities
urkud Jul 10, 2021
84a6bbb
Merge branch 'master' into change-origin
urkud Jul 11, 2021
20fbfbe
Snapshot
urkud Jul 11, 2021
67e29c7
Fix
urkud Jul 11, 2021
e755bc1
Fix, use notation
urkud Jul 11, 2021
da9e6c4
Fix
urkud Jul 11, 2021
d6e3882
Fix
urkud Jul 12, 2021
3a80cb9
Add docs
urkud Jul 12, 2021
64b002a
Merge branch 'master' into change-origin
urkud Jul 13, 2021
ca487ec
Snapshot
urkud Jul 13, 2021
dc0ccb7
Merge branch 'mul-le-mul' into change-origin
urkud Jul 13, 2021
9faa67a
speedup
sgouezel Jul 13, 2021
97537c3
use coercion
sgouezel Jul 13, 2021
6132c01
Merge remote-tracking branch 'origin/speedup_gromov' into change-origin
urkud Jul 13, 2021
7af6623
Merge branch 'master' into change-origin
urkud Jul 13, 2021
f2d7c7d
Update src/analysis/analytic/basic.lean
urkud Jul 13, 2021
c56100e
Merge branch 'master' into change-origin
urkud Jul 15, 2021
9bc04ed
Merge branch 'change-origin' of git://github.com/leanprover-community…
urkud Jul 15, 2021
eb57023
Fix docs and a whitespace
urkud Jul 17, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view