leanprover-community/mathlib3

Pull Requests Commits

feat(set/basic): additions to prod (#3943)

fpvandoorn committed 5 years ago

187bfa52

feat(*/category/*): add coe_of simp lemmas (#3938)

kim-em committed 5 years ago

fb6046ed

chore(*): trivial golfing using dec_trivial tactic (#3949)

jcommelin committed 5 years ago

206673e7

feat(finsupp/basic): add hom_ext (#3941)

kbuzzard committed 5 years ago

dd742dc8

fix(set_theory/game): remove stray #lint introduced in #3939 (#3948)

TwoFX committed 5 years ago

a31096de

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

leanprover-community-bot committed 5 years ago

da475484

feat(algebra/group/with_one): more API for with_zero (#3716)

kbuzzard committed 5 years ago

666a2e2e

feat(data/padic/padic_integers): homs to zmod(p ^ n) (#3882)

jcommelin committed 5 years ago

44787193

chore(set_theory/game): various cleanup and code golf (#3939)

TwoFX committed 5 years ago

b03ce616

feat(category_theory/adjunction): restrict adjunction to full subcategory (#3924)

b-mehta committed 5 years ago

878c44f1

feat(data/sigma/basic): cleanup (#3933)

fpvandoorn committed 5 years ago

a5a98587

doc(ring_theory/*): add some module docstrings (#3880)

kbuzzard committed 5 years ago

34093880

feat(combinatorics): define simple graphs (#3458)

jalex-stark committed 5 years ago

d4d33dea

refactor(geometry/euclidean): split up file (#3926)

jsm28 committed 5 years ago

8af15797

feat(algebra/add_torsor): vsub_vadd_comm (#3928)

jsm28 committed 5 years ago

1404ad83

feat(set_theory/game): grundy number of single-heap nim (#3930)

TwoFX committed 5 years ago

96b559c7

feat(category_theory/images): unique image (#3921)

b-mehta committed 5 years ago

1ccdbb9c

feat(category_theory): cancel fully faithful functor (#3920)

b-mehta committed 5 years ago

685d9dd3

chore(category_theory/conj): add a new simp lemma (#3922)

b-mehta committed 5 years ago

ebd3351b

feat(category_theory/adjunction): opposite adjunctions (#3899)

b-mehta committed 5 years ago

f2304096

feat(category_theory/limits/shapes/finite*): finite limits from limits (#3800)

b-mehta committed 5 years ago

bfc8c66b

feat(category_theory/fully_faithful): equivalence of homsets (#3923)

b-mehta committed 5 years ago

bf6cd285

feat(ring_theory/jacobson): Proof that if a ring is a Jacobson Ring then so is its localization at a single element (#3651)

dtumad committed 5 years ago

7d4f7730

feat(linear_algebra/affine_space): more lemmas (#3918)

jsm28 committed 5 years ago

e2167558

feat(geometry/euclidean): Monge point and orthocenter (#3872)

jsm28 committed 5 years ago

d80f3ef3

feat(tactic/*,meta/expr): refactor and extend binder matching functions (#3830)

JLimperg committed 5 years ago

588e46c6

refactor(linear_algebra/affine_space/basic): make more arguments of smul_vsub_vadd_mem implicit (#3917)

jsm28 committed 5 years ago

ffd86262

fix(data/sigma/basic): rename `ext` to `sigma.ext` (#3916)

urkud committed 5 years ago

7d88a30a

feat(data/finset/basic): insert_singleton_comm (#3914)

jsm28 committed 5 years ago

ff970553

feat(linear_algebra/finite_dimensional): Add `linear_equiv.of_inj_endo` and related lemmas (#3878)

abentkamp committed 5 years ago

7ac7246e

Newer Older