leanprover-community/mathlib3

Pull Requests Commits

urkud committed 5 years ago

bfa8752d

refactor(algebra/add_torsor): define pointwise `-ᵥ` and `+ᵥ` on sets (#4710)

urkud committed 5 years ago

03f0285d

feat(algebra/gcd_monoid): noncomputably defines `gcd_monoid` structures from partial information (#4664)

awainverse committed 5 years ago

4c4d47c2

Merge branch 'master' into bundle-direction

urkud committed 5 years ago

4f1e8c38

Merge branch 'affine-equiv' into mazur-ulam-affine

urkud committed 5 years ago

55d6d2eb

Merge branch 'master' into affine-equiv

urkud committed 5 years ago

e5e46c4b

urkud committed 5 years ago

8d90bba5

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

leanprover-community-bot committed 5 years ago

fca876ea

urkud committed 5 years ago

5f62c16b

feat(archive): formalize compiler correctness by McCarthy and Painter (#4702)

xiw committed 5 years ago

df450024

feat(linear_algebra/affine_space): define `affine_equiv` (#2909)

urkud committed 5 years ago

1b4e7694

Add simp lemmas

urkud committed 5 years ago

eab40bf3

Apply suggestions from code review

urkud committed 5 years ago

Verified 676cdd2b

chore(linear_algebra/basic): a few simp lemmas (#4727)

urkud committed 5 years ago

75316cad

urkud committed 5 years ago

6ae8edfd

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

leanprover-community-bot committed 5 years ago

01c1e6fb

fixup(category_theory/sites): add arrow sets that aren't sieves (#4703)

b-mehta committed 5 years ago

3a860cc4

Merge branch 'set-vsub' into bundle-direction

urkud committed 5 years ago

90b135f6

urkud committed 5 years ago

f36e46d1

chore(category_theory/limits/preserves): split up files and remove redundant defs (#4717)

b-mehta committed 5 years ago

857cbd52

Merge branch 'master' into bundle-direction

urkud committed 5 years ago

41da9b21

urkud committed 5 years ago

dd7074ca

urkud committed 5 years ago

d9d9a444

feat(data/complex/module): ![1, I] is a basis of C over R (#4713)

urkud committed 5 years ago

8489972a

Merge branch 'staging' of git://github.com/leanprover-community/mathlib into affine-equiv

urkud committed 5 years ago

f02136b1

Merge branch 'inj-lemmas' into affine-equiv

urkud committed 5 years ago

7c3c49c7

Merge commit 'fe9f3ea0f' into affine-equiv

urkud committed 5 years ago

c78d72ba

chore(*): review some lemmas about injectivity of coercions (#4711)

urkud committed 5 years ago

cf551ee3

chore(.gitignore): gitignore for emacs temp files (#4699)

lacker committed 5 years ago

5d52ea42

fix(tactic/norm_num): remove one_div from simp set (#4705)

digama0 committed 5 years ago

8131349c

Newer Older