leanprover-community/mathlib3

Pull Requests Commits

chore(category_theory): rename to category

kim-em committed 5 years ago

56030922

chore(category): rename to control

kim-em committed 5 years ago

1934b396

feat(data/list): more lemmas on joins and sums (#2501)

sgouezel committed 5 years ago

ee8451b9

chore(scripts): update nolints.txt (#2514)

leanprover-community-bot committed 5 years ago

6795c9df

feat(tactic/delta_instance): protect names and deal with functions (#2477)

robertylewis committed 5 years ago

3162c1c9

chore(scripts): update nolints.txt (#2510)

leanprover-community-bot committed 5 years ago

2f6b8d73

chore(topology/algebra/module): make `id` use explicit args (#2509)

urkud committed 5 years ago

7a718662

chore(*): add missing copyright headers (#2505)

kim-em committed 5 years ago

62feebc2

chore(tactic/*): remove some unused args in commands (#2498)

khoek committed 5 years ago

c8946c9d

docs(*): merge rewrite tactic tag into rewriting (#2512)

robertylewis committed 5 years ago

00d7da20

chore(data/list/*): various renamings to use dot notation (#2481)

urkud committed 5 years ago

13393e3c

feat(linear_algebra): quadratic forms (#2480)

Vierkantor committed 5 years ago

3ae22de4

chore(tactic/pi_instance): add a docstring, remove a little bit of redundancy (#2500)

khoek committed 5 years ago

e7bd3127

feat(algebra): define `invertible` typeclass (#2504)

Vierkantor committed 5 years ago

b7af2838

feat(cmd/simp): let `#simp` use declared `variables` (#2478)

khoek committed 5 years ago

02d73084

chore(scripts): update nolints.txt (#2503)

leanprover-community-bot committed 5 years ago

01967486

doc(tactic/*): doc entries for some missing tactics (#2489)

robertylewis committed 5 years ago

fdbf22d7

feat(data/string): add docstrings and improve semantics (#2497)

khoek committed 5 years ago

fc7ac675

feat(data/string): add phrasings common to conventional languages (#2493)

khoek committed 5 years ago

9ccfa926

chore(*): remove unnecessary transitive imports (#2496)

kim-em committed 5 years ago

64e464f1

chore(tactic/suggest): add a docstring (#2499)

khoek committed 5 years ago

8a7b94fb

feat(category_theory/epi_mono): opposite epi mono properties (#2479)

b-mehta committed 5 years ago

7c10fd2b

feat(category_theory): wide pullbacks and limits in the over category (#2461)

b-mehta committed 5 years ago

4d94de48

chore(scripts): update nolints.txt (#2495)

leanprover-community-bot committed 5 years ago

4dadd26d

chore(tactic/apply_fun): add doc string and remove duplication (#2485)

khoek committed 5 years ago

bcbdebaa

chore(scripts): update nolints.txt (#2494)

leanprover-community-bot committed 5 years ago

691a230f

feat(mk_iff_of_inductive_prop): add, use, and document command (#2490)

robertylewis committed 5 years ago

2fb6022e

chore(*): only import one file per line (#2470)

kim-em committed 5 years ago

591a0a00

chore(scripts): update nolints.txt (#2491)

leanprover-community-bot committed 5 years ago

8865b00a

chore(tactic/auto_cases): add docstring and remove duplication (#2488)

khoek committed 5 years ago

d40662f5

Older