Merge #1099
amswerdlow
merged
306 commits into
inner_product_spaces
from
master
feat(algebra/field_power): add fpow_one, one_fpow, fpow_mul, mul_fpow…
8838ff35
feat(scripts/cache_olean): cache and fetch olean binaries (#766)
25bab564
refactor(*): unify group/monoid_action, make semimodule extend action…
179d4d08
feat(category_theory/instances): category of groups (#749)
48df3219
fix(scripts/update-mathlib): update-mathlib shouldn't need github aut…
1c04a329
fix(scripts/update-mathlib): github authentication
6cd336cb
fix(scripts/update-mathlib): fix imports of python files
59caf112
feat(library_search): a simple library_search function (#839)
a4fd55ca
fix(scripts/deploy_nightly): pushing to the `lean-3.4.2` branch is so…
2e7f0099
fix(scripts/remote-install-update-mathlib): add GitPython dependency …
171e913a
feat(analysis/convex): convex sets and functions (#834)
dc7de460
refactor(data/zsqrtd/basic): move zsqrtd out of pell and into data (#…
c2bb4c5c
feat(data/polynomial): eval₂_neg
e1c035da
feat(data/complex/basic): smul_re,im
72634d2c
feat(data/finset): to_finset_eq_empty
514de772
feat(computability): computable_iff_re_compl_re
359cac1b
refactor(computability): unpack fixed_point proof
9480df50
fix(ring_theory/algebra): remove duplicate theorems to fix build
c91e6c2e
feat(data/real/pi): Compute the first three digits of pi (#822)
2851236b
fix(scripts/cache-olean): only run the post-checkout hook if we actua…
3bc0f00a
refactor(analysis/convex): make instance local (#869)
a1fe39b1
docs(tactics): minor rewrite of exactI, resetI etc
59e05930
docs(tactics): add introduction to the instance cache tactic section
867661e0
add tutorial about zmod37 (#767)
404e2c93
feat(category_theory): working in Sort rather than Type (#824)
2f088fc1
fix(build): prevent leanchecker from timing out
5995d460
feat(tactic/push_neg): a tactic pushing negations (#853)
5fe470bb
fix(tactic/congr'): some `\iff` goals were erroneously rejected
ec0a4ea1
Merge branch 'congr-2'
8e4542da
feat(data/nat/basic): nat.le_rec_on (#585)
5694d152
fix(build): improve compatibility of caching scripts with Sourcetree …
727120cc
Inductive limit of metric spaces (#732)
f385ad6b
fix(scripts/update-mathlib): protect file operations from interrupts …
7eac1785
feat(tactic/local_cache): add tactic-block-local caching mechanism (#…
13034ba3
build(travis): interrupt the build at the first error message (#708)
6c559892
chore(.travis.yml): use Lean to determine the Lean version (#714)
ce92e8af
fix(int/basic): change order of instances to int.cast (#877)
e96d6b75
feat(tactic/basic): add `tactic.get_goal` (#876)
f1120769
feat(algebra/pointwise): pointwise addition and multiplication of set…
7043a4ab
feat(topology/uniform_space/pi): indexed products of uniform spaces (…
c3aba261
feat(topology/metric_space/completion): completion of metric spaces (…
b9e9328e
feat(ring_theory/algebra_operations): submodules form a semiring (#856)
2c735dc9
feat(data/fin): add `fin.clamp` (#874)
a0cbe3be
chore(github/pr): mergify configuration (#871)
542d1790
fix(README): fix mergify icon
840ddeb7
chore(mergify): disable `delete_head_branch`
2230934a
chore(mergify): use team names instead of user names
d4fd4b2b
chore(mergify): fix config file
7762bc4f
chore(mergify): fix config
1c69b609
fix(build): fix Lean version
07aa1e3e
feat (analysis/normed_space/basic.lean): implement reverse triangle i…
384c9be2
feat(data/list/perm): nil_subperm (#882)
8183a5a6
chore(github/pr): enable code owners
3abfda0e
feat(algebra/char_p,field_theory/finite_card): cardinality of finite …
7aaccae7
chore(mergify): delete head branch when merging
b6c2be42
feat(category_theory): introduce the core of a category (#832)
0b7ee1b4
feat(data/matrix): more basic matrix lemmas (#873)
858d111c
feat(data/list/min_max): minimum and maximum over list (#884)
901bdbf4
feat(list.split_on): [1,1,2,3,2,4,4].split_on 2 = [[1,1],[3],[4,4]] (…
44d1c7aa
feat(data/mllist): monadic lazy lists (#865)
78a08ebc
fix(scripts): not all files were deployed through the curl command
d9ec8a82
fix(scripts): Mac Python's test support doesn't work on Travis
e809df6d
fix(scripts): protect `leanpkg test` against timeouts
d0f86077
fix(build): match build names
e0e231da
feat(algebra/opposites): opposites of operators (#538)
d8a2bc51
more general hypotheses for integer induction (#885)
3360f98a
feat(category_theory/bifunctor): simp lemmas (#867)
8d45ccb7
fix(scripts): not all files were deployed through the curl command (#…
8fa071f4
chore(mergify): require the AppVeyor build to succeed
8831e0a7
refactor(analysis/normed_space/bounded_linear_maps): nondiscrete norm…
ae8a1fb6
fix(appveyor): build every commit
53e7d724
refactor(analysis/normed_space/bounded_linear_maps): nondiscrete norm…
31ff5c5c
fix(analysis/normed_space/bounded_linear_maps): fix build (#895)
e4d3ca31
fix(build): external PRs can't use GitHub credentials
3000f328
feat(data/nat/basic): b = c if b - a = c - a (#862)
7e70ebd0
feat(field_theory/subfield): is_subfield instances (#891)
bd524fc1
feat(subgroup, subring, subfield): directed Unions of subrings are su…
891c0506
feat(data/list/min_max): add minimum (#892)
483a6c23
fix(category_theory): turn `has_limits` classes into structures (#896)
0a490302
trying to work out what was wrong with catching signals (#898)
5d81ab17
feat(topology/gromov_hausdorff): the Gromov-Hausdorff space (#883)
4fecb101
feat(analysis/complex/polynomial): fundamental theorem of algebra (#851)
10490ea7
feat(linear_algebra/dual): add dual vector spaces (#881)
5f1329a2
fix(doc/extra/tactic_writing): rename mul_left (#902) [ci skip]
6d2cf4ae
feat(category_theory/colimits): missing simp lemmas (#894)
ec51b6e1
feat(group_theory/subgroup): subtype.add_comm_group (#903)
29507a4b
feat(order/lexicographic): lexicographic pre/partial/linear orders (#…
eb024dc8
refactor(*): rename is_group_hom.mul to map_mul (#911)
66a86ffe
fix(mergify): require travis "push" check to push (#913)
c2d79f85
chore(build): allow PRs from separate repos to test deployment scripts
5c4f5f20
feat(field_theory/subfield): subfields are fields (#888)
4494001d
reorganising category_theory/instances/rings.lean (#909)
d692499e
refactor(category_theory): rename `functor.on_iso` to `functor.map_is…
96d748eb
feat(data/set/basic): inclusion map (#906)
f1683a9e
refactor(algebra/group): is_monoid_hom extends is_mul_hom (#915)
86bd577c
feat(category_theory): iso_whisker_(left|right) (#908)
f04535de
fix(category_theory): make the `nat_trans` arrow `⟹` a synonym for th…
89924726
refactor(order/lexicographic): use prod.lex and psigma.lex (#914)
49ccc9f7
fix(mergify): merge if either push or pr build passes. (#918)
c4b65da1
rename has_sum and is_sum to summable and has_sum (#912)
41014e50
feat(analysis/normed_space/deriv): show that the differential is uniq…
f5d43a95
minor changes (#921)
22fcb4e9
fix(tactic/explode): more accurate may_be_proof (#924)
c1e07a2e
feat(submonoid, subgroup, subring): is_ring_hom instances for set.inc…
36f0c224
refactor(data/int/basic): weaken hypotheses for int.induction_on (#887)
be79f25b
feat(algebra/free): free magma, semigroup, monoid (#735)
3fe449e1
fix(algebra.field): introduce division_ring_has_div' (#852)
49c3a049
docs(elan): remove reference to nightly Lean (#928)
f01934c6
fix(algebra/big_operators): change variables in finset.prod_map to re…
a1b7dcdf
feat(scripts): disable testing the install scripts in external PRs (#…
ca5d4c1f
feat(topology/algebra/continuous_functions): the ring of continuous f…
d06eb858
feat(nat/basic): add some basic nat inequality lemmas (#937)
5f04e76e
feature(category_theory/instances/Top/open[_nhds]): category of open …
361e2163
feat(data/set/intervals): some interval lemmas (#942)
8985a433
feat(data/finset): powerset_len (subsets of a given size) (#899)
22948763
feat(*): various additions to low-level files (#904)
7bbbee1e
fix(test/local_cache): make the trace text explicit and quiet (#941)
4b8106b3
feat(tactic/omega): tactic for linear integer & natural number arithm…
3f4b154a
feat(scripts): use apt-get on ubuntu and support older Python version…
8b23dadc
feat(analysis/normed_space): more facts about operator norm (#927)
032400bd
feat(group_theory/subgroup): additive version of inj_iff_trivial_ker …
d0140dd8
style(tactic/omega): whitespace and minor tweaks
c1aff1b5
feat(tactic/ring): treat expr atoms up to defeq (#949)
e4fc5afd
fix(topology/order): Missing Prop annotation (#952)
784a68c3
feat(tactic/linarith): treat expr atoms up to defeq (#950)
7370cbf2
feat(data/[fin]set): add some more basic properties of (finite) sets …
4b9d94dc
feat(tactic/clear_except): clear most of the assumptions in context (…
9daa1a57
fix(tactic/interactive): allow `convert e using 0`
3478f1f6
feat(data/list/basic): index_of_inj (#954)
63bbd1c3
refactor(data/equiv/basic): simplify definition of equiv.set.range (#…
45456cf1
fix(ring_theory/adjoin_root): move adjoin_root out of adjoin_root nam…
0d7b4195
feat(function/embedding): ext and ext_iff (#962)
1d9ff681
refactor(analysis/normed_space/operator_norm): replace subspace with …
038f809c
feat(data/equiv/basic): sum_compl_apply and others (#961)
0444f9c2
fix(README): update maintainer list
b49bf61c
refactor(analysis/normed_space): use bundled type for `fderiv` (#956)
53f98786
Update elan.md
9b3e91b0
refactor(tactic/interactive): remove dependencies of (#878)
00aaf05a
feat(analysis/normed_space): open mapping (#900)
8dcce05f
fix(scripts/remote-install-update-mathlib): missing dependency (#964)
a15fca5d
fix(scripts/remote-install-update-mathlib): try again [ci skip]
7c868148
chore(category_theory): move small_category_of_preorder to preorder n…
c8a2aa95
feat(script/auth_github): improve messages [ci skip] (#965)
b3433a51
feat(category_theory/limits): complete lattices have (co)limits (#931)
9b7fb5fd
fix(tactic/library_search): iff lemmas with universes (#935)
69094fcf
feat(category_theory/limits/opposites): (co)limits in opposite catego…
ef11fb3d
feat(ring_theory/ideal_operations): inj_iff_trivial_ker for ring homo…
8a097f13
fix(script/remote-install-update-mathlib) fix answer reading and requ…
d2889058
fix(scripts/remote-install-update-mathlib): apt shouldn't ask (#969)
60b3c198
fix(data/polynomial): change instance order in polynomial.subsingleto…
6956daa2
remove code duplication (#971)
3eb7ebca
chore(docs): delete docs/wip.md (#972)
44386cde
chore(travis): disable the check for minimal imports (#973)
219cb1a1
feat(category_theory/limits): support for special shapes of (co)limit…
f5060c40
feat(docs/install_debian): Debian startup guide (#974)
f2db6369
chore(README): put the badges in the README on one line (#975)
e747c91c
chore(build): build only master and its related PRs
7b1105bf
feat(tactic/decl_mk_const): performance improvement for library_searc…
f98ffdef
feat(option/injective_map) (#978)
c7baf8ef
feat(colimits): arbitrary colimits in Mon and CommRing (#910)
b4d483e2
feat(logic/basic): forall_iff_forall_surj (#977)
7dea60ba
fix(data/set/finite): make fintype_seq an instance (#979)
fbce6e4d
feat(data/set/basic): prod_subset_iff (#980)
fc8b08b3
feat(presheaves) (#886)
1e8f438c
feat(category_theory/products): associators (#982)
3f26ba88
feat(ring_theory/adjoin): adjoining elements to form subalgebras (#756)
23270e71
six(style.md): fix broken code (#987)
f536dac8
feat(category_theory): currying for functors (#981)
6eba20b0
chore(build): build against Lean 3.5 nightly build (#989)
505f748b
chore(build): fix stages in cron job
98ba07bc
feat(category/monad/cont): monad_cont instances for state_t, reader_t…
c726c128
chore(build): cron build restarts from scratch
717033e3
feat(scripts): add --build-new flag to cache-olean (#992)
4a38d2e1
building the hyperreal library (#835)
820bac36
feat(category_theory/category_of_elements) (#990)
87cf6e36
feat(group_theory/subgroup): is_subgroup.inter (#994)
73a30da3
chore(tactics): splitting tactics and tests into more files (#985)
c9cfafc9
feat(*): preorder instances for with_bot and with_zero (#996)
7f9717fd
refactor(order/basic): make type class args explicit in {*}order.lift…
8f5d2401
refactor(strict_mono): make definition + move to order_functions (#998)
df5eddeb
feat(algebra/pointwise): More lemmas on pointwise multiplication (#997)
5329bf3a
feat(set_theory): add to cardinal, ordinal, cofinality (#963)
e66e1f30
fix(tactic/basic): missing `conv` from tactic.basic (#1004)
91a7fc23
fix(category/fold): use correct `opposite` (#1008)
6858c2f7
refactor(algebra/associated): rename nonzero_of_irreducible to ne_zer…
8603e6b0
feat(data/polynomial): degree_eq_one_of_irreducible_of_root (#1010)
60da4f4d
chore(compatibility): compatibility with Lean 3.5.0c (#1007)
c7d870e8
docs(algebra/ring): document compatibility hack [skip ci]
e6d959df
chore(build): remove script testing on PRs [skip ci]
8e71ceec
fix(docs/*): docs reorganization [skip ci] (#1012)
a154dedc
feat(logic/function): comp₂ -- useful for binary operations (#993)
de5d0387
feat(topology/maps): closed embeddings (#1013)
1e0761e5
feat(category_theory): lemmas about cancellation (#1005)
48645152
chore(scripts): migrate scripts to own repo (#1011)
e42d808b
chore(Github): no need to wait for Appveyor anymopre
b9b5bb4b
feat(Top.presheaf_ℂ): presheaves of functions to topological commutat…
70cd00bc
document the change in scripts (#1024)
82f151f5
feat(category_theory/iso): missing lemmas (#1001)
6c35df0d
feat(category_theory/products): missing simp lemmas (#1003)
c8a0bb6b
feat(tactics/interactive): choose uses exists_prop (#1014)
01b345c1
feat(data/equiv/basic): equiv.nonempty_iff_nonempty (#1020)
f8385b19
feat(topology/constructions): topology of sum types (#1016)
07ba43ee
feat(algebra/order_functions): generalize strict_mono.monotone (#1022)
6dc06824
feat(category_theory/opposites): iso.op (#1021)
cefb9d43
squeeze_simp (#1019)
a72641be
feat(analysis/normed_space/deriv): more material on derivatives (#966)
ade99c8c
fix(data/multiset): remove duplicate setoid instance (#1027)
fe19bdb4
feat(tactic): new tactics to normalize casts inside expressions (#988)
22790e06
fix(docs/tactics): fix layout, remove noise
02857d56
feat(data/equiv/functor): map_equiv (#1026)
e7b64c55
feat(data/nat/basic): decreasing induction (#1031)
ae8f197b
feat(category_theory): adjoint equivalences and limits under equivale…
7b579b79
feat(tactic/terminal_goal): determine if other goals depend on the cu…
3022cafd
refactor(topology): change continuous_at_within to continuous_within_…
136e67a6
feat(category_theory): monos and epis in Type and Top (#1030)
b5aae18a
chore(*): reduce imports (#1033)
c75c096a
fix(data/nat/enat): Fix typo in lemma name (#1037)
ad0f42df
feat(data/nat/basic): make decreasing induction eliminate to Sort (#1…
def48b06
chore(opposites): merge two definitions of `opposite` (#1036)
96ea9b99
fix(data/complex/exponential): make complex.exp irreducible (#1040)
a6c1f377
feat(tactic/basic): add tactic.rewrite, and sort list (#1039)
f633c948
refactor: change variables order in some composition lemmas (#1035)
0b350228
feat(set_theory/surreal): surreal numbers (#958)
901178e2
fix(topology/stone_cech): faster proof from @PatrickMassot (#1042)
45afa86e
feat(adjointify): make definition easier for elaborator (#1045)
5e5298b9
refactor(data/complex/exponential): improve trig proofs (#1041)
fa0e7570
feat(tactic/squeeze): remove noise from output (#1047)
73c3f717
feat(topology/order): make nhds irreducible (#1043)
b9cb69c3
refactor(topology/metric/gromov_hausdorff): make Hausdorff_edist irre…
cb4c9ee7
refactor: coherent composition order (#1055)
f2534017
feat(tactic/linarith): better input syntax linarith only [...] (#1056)
d4c7b7a6
feat(topology/opens): continuous.comap : opens Y → opens X (#1061)
15a6af22
feat(tactic/basic): adds `contrapose` tactic (#1015)
d001abfd
chore(ring_theory/algebra): simp-lemmas for alg_hom.to_linear_map (#1…
593938cd
chore(topology/algebra/monoid): continuous_mul_left/right (#1065)
8cf7c4c8
feat(category_theory): limits in CommRing (#1006)
0ab8a89d
feat(algebra/pi_instances): product of submonoids/groups/rings (#1066)
cb30c97e
refactor(integration.lean): changing `measure_space` to `measurable_s…
34613996
feat(*): image_closure (#1069)
971ddcc2
feat(data/nat): various lemmas (#1017)
f004d327
feat(linear_algebra/basic): general_linear_group basics (#1064)
d07e3b3e
doc(finsupp,category_theory): fixes (#1075)
15fecbdd
chore(CommRing/adjunctions): refactor proofs (#1049)
62acd6b8
refactor(set_theory/ordinal): shorten proof of well_ordering_thm (#1078)
c6a7f300
feat(group_theory/conjugates) : define conjugates (#1029)
d4343972
fix(tactic/rcases): add parse desc to rcases/rintro (#1091)
b20b722b
feat(ordered_group): add missing instance (#1094)
0de4bba3
feat(presheaves/stalks): stalks of presheafs, and presheafed spaces w…
d935bc31
feat(ring_theory): free_ring and free_comm_ring (#734)
4845b663
feat(category_theory/monoidal): monoidal categories, monoidal functor…
c49ac06f
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Milestone
No milestone
Login to write a write a comment.
Login via GitHub