leanprover-community/mathlib

Pull Requests Commits

feat(analysis/normed_space/operator_norm): a few more estimates (#2233)

urkud committed 5 years ago

Verified 67327881

chore(scripts/deploy_docs.sh): skip gen_docs if already built (#2263)

bryangingechen committed 5 years ago

Verified 1b13ccdf

chore(data/int/basic): change instance order (#2257)

sgouezel committed 5 years ago

Verified 211c5d11

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

3c0b35c4

feat(algebra/ring): generalize mul_ite (#2223)

kim-em committed 5 years ago

Verified d0a85073

feat(logic/basic): trivial transport lemmas (#2254)

kim-em committed 5 years ago

Verified 786c7375

chore(tactic/lint): typo (#2253)

kim-em committed 5 years ago

Verified 451de279

chore(tactic/*): update tags (#2224)

robertylewis committed 6 years ago

Verified 21ad1d3a

chore(ci): update nolints before docs and leanchecker (#2250)

robertylewis committed 6 years ago

Verified d3cbd4d0

chore(.mergify.yml): cleanup (#2248)

bryangingechen committed 6 years ago

Verified de39b9a8

doc(docs/install/project.md): mention that projects are git repositories (#2244)

bryangingechen committed 6 years ago

Verified 2fbf0070

feat(data/equiv/local_equiv): construct from `bij_on` or `inj_on` (#2232)

urkud committed 6 years ago

Verified 75b4ee86

feat(topology/algebra/module): define `fst` and `snd`, review (#2247)

urkud committed 6 years ago

Verified 8943351e

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

5b443634

refactor(data/set/function): move `function.restrict` to `set`, redefine (#2243)

urkud committed 6 years ago

Verified 0fc4e6a8

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

fa36a8ef

feat(data/equiv/functor): bifunctor.map_equiv (#2241)

kim-em committed 6 years ago

Verified ea10e173

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

ab33237d

feat(tactic/squeeze): improve suggestion of `cases x; squeeze_simp` (#2218)

cipher1024 committed 6 years ago

Verified dbc4284c

chore(tactic/solve_by_elim): refactor (#2222)

kim-em committed 6 years ago

Verified 30146a02

chore(ci): only run on push (#2237)

robertylewis committed 6 years ago

Verified 2755eaea

feat(algebra/homology): chain complexes (#2174)

kim-em committed 6 years ago

Verified 6e6c81a4

feat(topology/metric_space/isometry): add_left/right, neg (#2234)

urkud committed 6 years ago

Verified e04892ec

feat(topology/local_homeomorph): a few facts about `local_homeomorph` (#2231)

urkud committed 6 years ago

Verified bb01537b

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

05aa9556

feat(*): a few more theorems about `unique` and `subsingleton` (#2230)

urkud committed 6 years ago

Verified bedb810b

feat(data/equiv): pi_congr (#2204)

kim-em committed 6 years ago

Verified 1eae0be1

chore(README): add Bryan; alphabetize (#2238)

robertylewis committed 6 years ago

Verified 83014bf7

chore(algebra/ordered_field): merge `inv_pos` / `zero_lt_inv` with `inv_pos'` / `inv_neg` (#2226)

urkud committed 6 years ago

Verified d9083bcb

feat(tactic/core): trace_if_enabled (#2209)

kim-em committed 6 years ago

Verified 24b82c91

Newer Older