PR #1099 Merge - SemanticDiff

feat(algebra/field_power): add fpow_one, one_fpow, fpow_mul, mul_fpow (closes #855)

johoelzl committed 6 years ago

feat(scripts/cache_olean): cache and fetch olean binaries (#766)

cipher1024 committed 6 years ago

refactor(*): unify group/monoid_action, make semimodule extend action (#850)

ChrisHughes24 committed 6 years ago

feat(category_theory/instances): category of groups (#749)

rwbarton committed 6 years ago

fix(scripts/update-mathlib): update-mathlib shouldn't need github authentication

cipher1024 committed 6 years ago

fix(scripts/update-mathlib): github authentication

cipher1024 committed 6 years ago

fix(scripts/update-mathlib): fix imports of python files

cipher1024 committed 6 years ago

feat(library_search): a simple library_search function (#839)

cipher1024 committed 6 years ago

fix(scripts/deploy_nightly): pushing to the `lean-3.4.2` branch is sometimes blocked (#859)

cipher1024 committed 6 years ago

fix(scripts/remote-install-update-mathlib): add GitPython dependency (#860)

cipher1024 committed 6 years ago

feat(analysis/convex): convex sets and functions (#834)

avigad committed 6 years ago

refactor(data/zsqrtd/basic): move zsqrtd out of pell and into data (#861)

ChrisHughes24 committed 6 years ago

feat(data/polynomial): eval₂_neg

ChrisHughes24 committed 6 years ago

feat(data/complex/basic): smul_re,im

digama0 committed 6 years ago

feat(data/finset): to_finset_eq_empty

digama0 committed 6 years ago

feat(computability): computable_iff_re_compl_re

digama0 committed 6 years ago

refactor(computability): unpack fixed_point proof

digama0 committed 6 years ago

fix(ring_theory/algebra): remove duplicate theorems to fix build

robertylewis committed 6 years ago

feat(data/real/pi): Compute the first three digits of pi (#822)

digama0 committed 6 years ago

fix(scripts/cache-olean): only run the post-checkout hook if we actually changed branches (#857)

cipher1024 committed 6 years ago

refactor(analysis/convex): make instance local (#869)

digama0 committed 6 years ago

docs(tactics): minor rewrite of exactI, resetI etc

PatrickMassot committed 6 years ago

docs(tactics): add introduction to the instance cache tactic section

PatrickMassot committed 6 years ago

add tutorial about zmod37 (#767)

PatrickMassot committed 6 years ago

feat(category_theory): working in Sort rather than Type (#824)

rwbarton committed 6 years ago

fix(build): prevent leanchecker from timing out

cipher1024 committed 6 years ago

feat(tactic/push_neg): a tactic pushing negations (#853)

cipher1024 committed 6 years ago

fix(tactic/congr'): some `\iff` goals were erroneously rejected

cipher1024 committed 6 years ago

Merge branch 'congr-2'

cipher1024 committed 6 years ago

feat(data/nat/basic): nat.le_rec_on (#585)

avigad committed 6 years ago

fix(build): improve compatibility of caching scripts with Sourcetree (#863)

cipher1024 committed 6 years ago

Inductive limit of metric spaces (#732)

avigad committed 6 years ago

fix(scripts/update-mathlib): protect file operations from interrupts (#864)

cipher1024 committed 6 years ago

feat(tactic/local_cache): add tactic-block-local caching mechanism (#837)

cipher1024 committed 6 years ago

build(travis): interrupt the build at the first error message (#708)

cipher1024 committed 6 years ago

chore(.travis.yml): use Lean to determine the Lean version (#714)

cipher1024 committed 6 years ago

fix(int/basic): change order of instances to int.cast (#877)

cipher1024 committed 6 years ago

feat(tactic/basic): add `tactic.get_goal` (#876)

cipher1024 committed 6 years ago

feat(algebra/pointwise): pointwise addition and multiplication of sets (#854)

digama0 committed 6 years ago

feat(topology/uniform_space/pi): indexed products of uniform spaces (#845)

robertylewis committed 6 years ago

feat(topology/metric_space/completion): completion of metric spaces (#743)

digama0 committed 6 years ago

feat(ring_theory/algebra_operations): submodules form a semiring (#856)

digama0 committed 6 years ago

feat(data/fin): add `fin.clamp` (#874)

cipher1024 committed 6 years ago

chore(github/pr): mergify configuration (#871)

cipher1024 committed 6 years ago

fix(README): fix mergify icon

ChrisHughes24 committed 6 years ago

chore(mergify): disable `delete_head_branch`

cipher1024 committed 6 years ago

chore(mergify): use team names instead of user names

cipher1024 committed 6 years ago

chore(mergify): fix config file

cipher1024 committed 6 years ago

chore(mergify): fix config

cipher1024 committed 6 years ago

fix(build): fix Lean version

cipher1024 committed 6 years ago

feat (analysis/normed_space/basic.lean): implement reverse triangle inequality (#831)

mergify[bot] committed 6 years ago

feat(data/list/perm): nil_subperm (#882)

mergify[bot] committed 6 years ago

chore(github/pr): enable code owners

cipher1024 committed 6 years ago

feat(algebra/char_p,field_theory/finite_card): cardinality of finite fields (#819)

mergify[bot] committed 6 years ago

chore(mergify): delete head branch when merging

cipher1024 committed 6 years ago

feat(category_theory): introduce the core of a category (#832)

mergify[bot] committed 6 years ago

feat(data/matrix): more basic matrix lemmas (#873)

mergify[bot] committed 6 years ago

feat(data/list/min_max): minimum and maximum over list (#884)

mergify[bot] committed 6 years ago

feat(list.split_on): [1,1,2,3,2,4,4].split_on 2 = [[1,1],[3],[4,4]] (#866)

mergify[bot] committed 6 years ago

feat(data/mllist): monadic lazy lists (#865)

mergify[bot] committed 6 years ago

fix(scripts): not all files were deployed through the curl command

cipher1024 committed 6 years ago

fix(scripts): Mac Python's test support doesn't work on Travis

cipher1024 committed 6 years ago

fix(scripts): protect `leanpkg test` against timeouts

cipher1024 committed 6 years ago

fix(build): match build names

cipher1024 committed 6 years ago

feat(algebra/opposites): opposites of operators (#538)

rwbarton committed 6 years ago

more general hypotheses for integer induction (#885)

mergify[bot] committed 6 years ago

feat(category_theory/bifunctor): simp lemmas (#867)

mergify[bot] committed 6 years ago

fix(scripts): not all files were deployed through the curl command (#879)

cipher1024 committed 6 years ago

chore(mergify): require the AppVeyor build to succeed

cipher1024 committed 6 years ago

refactor(analysis/normed_space/bounded_linear_maps): nondiscrete normed field

avigad committed 6 years ago

fix(appveyor): build every commit

cipher1024 committed 6 years ago

refactor(analysis/normed_space/bounded_linear_maps): nondiscrete normed field

avigad committed 6 years ago

fix(analysis/normed_space/bounded_linear_maps): fix build (#895)

ChrisHughes24 committed 6 years ago

fix(build): external PRs can't use GitHub credentials

cipher1024 committed 6 years ago

feat(data/nat/basic): b = c if b - a = c - a (#862)

mergify[bot] committed 6 years ago

feat(field_theory/subfield): is_subfield instances (#891)

ChrisHughes24 committed 6 years ago

feat(subgroup, subring, subfield): directed Unions of subrings are subrings (#889)

mergify[bot] committed 6 years ago

feat(data/list/min_max): add minimum (#892)

robertylewis committed 6 years ago

fix(category_theory): turn `has_limits` classes into structures (#896)

mergify[bot] committed 6 years ago

trying to work out what was wrong with catching signals (#898)

mergify[bot] committed 6 years ago

feat(topology/gromov_hausdorff): the Gromov-Hausdorff space (#883)

cipher1024 committed 6 years ago

feat(analysis/complex/polynomial): fundamental theorem of algebra (#851)

mergify[bot] committed 6 years ago

feat(linear_algebra/dual): add dual vector spaces (#881)

robertylewis committed 6 years ago

fix(doc/extra/tactic_writing): rename mul_left (#902) [ci skip]

robertylewis committed 6 years ago

feat(category_theory/colimits): missing simp lemmas (#894)

mergify[bot] committed 6 years ago

feat(group_theory/subgroup): subtype.add_comm_group (#903)

ChrisHughes24 committed 6 years ago

feat(order/lexicographic): lexicographic pre/partial/linear orders (#820)

mergify[bot] committed 6 years ago

refactor(*): rename is_group_hom.mul to map_mul (#911)

ChrisHughes24 committed 6 years ago

fix(mergify): require travis "push" check to push (#913)

cipher1024 committed 6 years ago

chore(build): allow PRs from separate repos to test deployment scripts

cipher1024 committed 6 years ago

feat(field_theory/subfield): subfields are fields (#888)

mergify[bot] committed 6 years ago

reorganising category_theory/instances/rings.lean (#909)

mergify[bot] committed 6 years ago

refactor(category_theory): rename `functor.on_iso` to `functor.map_iso` (#893)

mergify[bot] committed 6 years ago

feat(data/set/basic): inclusion map (#906)

mergify[bot] committed 6 years ago

refactor(algebra/group): is_monoid_hom extends is_mul_hom (#915)

mergify[bot] committed 6 years ago

feat(category_theory): iso_whisker_(left|right) (#908)

mergify[bot] committed 6 years ago

fix(category_theory): make the `nat_trans` arrow `⟹` a synonym for the `hom` arrow (#907)

mergify[bot] committed 6 years ago

refactor(order/lexicographic): use prod.lex and psigma.lex (#914)

ChrisHughes24 committed 6 years ago

fix(mergify): merge if either push or pr build passes. (#918)

ChrisHughes24 committed 6 years ago

rename has_sum and is_sum to summable and has_sum (#912)

mergify[bot] committed 6 years ago

mathlib3 Merge #1099 Merged

mathlib3
Merge
#1099

Merged