leanprover-community/mathlib3

Pull Requests Commits

feat(README): add @Vierkantor to maintainer list (#3674)

robertylewis committed 5 years ago

d3e1f5fb

feat(linear_algebra/affine_space): simplex ext lemmas (#3669)

jsm28 committed 5 years ago

d6c17c94

feat(algebra/category/Module): the category of R-modules is abelian (#3606)

kim-em committed 5 years ago

60ba4782

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

leanprover-community-bot committed 5 years ago

fb883ea5

chore(analysis/calculus/times_cont_diff): transpose lemmas (#3665)

hrmacbeth committed 5 years ago

06df5038

chore(group_theory/*): refactor quotient groups to use bundled subgroups (#3321)

kim-em committed 5 years ago

4588400f

feat(order/filter/lift): a few lemmas about `filter.lift' _ powerset` (#3652)

urkud committed 5 years ago

65598321

feat(category_theory/limits): transporting is_limit (#3598)

kim-em committed 5 years ago

fe4da7bc

feat(category_theory): Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D (#3576)

kim-em committed 5 years ago

52c0b421

feat(category_theory): braided and symmetric categories (#3550)

kim-em committed 5 years ago

e99518b2

feat(linear_algebra/tensor_algebra): Tensor algebras (#3531)

adamtopaz committed 5 years ago

8c1e2da7

feat(dynamics/periodic_pts): definition and basic properties (#3660)

urkud committed 5 years ago

58f2c36a

feat(data/set/intervals): define `set.ord_connected` (#3647)

urkud committed 5 years ago

78655b6e

chore(algebra/order): enable dot syntax (#3643)

urkud committed 5 years ago

f2db6a8f

feat(algebra/category/*): forget reflects isos (#3600)

kim-em committed 5 years ago

6394e4d4

feat(measure_theory): cleanup and generalize measure' (#3648)

fpvandoorn committed 5 years ago

d76c75e9

feat(analysis/calculus/times_cont_diff): inversion is smooth (#3639)

hrmacbeth committed 5 years ago

fc65ba0d

feat(topology/local_homeomorph): open_embedding.continuous_at_iff (#3599)

kim-em committed 5 years ago

d3de289a

chore(*): bump to Lean 3.18.4 (#3610)

robertylewis committed 5 years ago

4274dddf

feat(order/filter/extr, topology/local_extr): links between extremas of two eventually le/eq functions (#3624)

ADedecker committed 5 years ago

92a20e64

chore(order/filter/bases): generalize `has_basis.restrict` (#3645)

urkud committed 5 years ago

aa673157

feat(topology/subset_properties): add `is_compact.induction_on` (#3642)

urkud committed 5 years ago

c6f33994

feat(complete_lattice): put supr_congr and infi_congr back (#3646)

fpvandoorn committed 5 years ago

37ab4263

chore(*): assorted small lemmas (#3644)

urkud committed 5 years ago

7e570ed1

feat(analysis/calculus/fderiv): inversion is differentiable (#3510)

hrmacbeth committed 5 years ago

396a764f

fix(tactic/simps): do not reach unreachable code (#3637)

TwoFX committed 5 years ago

3ae893dc

feat(group_theory/subgroup): Add `mem_infi` and `coe_infi` (#3634)

eric-wieser committed 5 years ago

f78a012d

ci(fetch_olean_cache.sh): error handling (#3628)

PatrickMassot committed 5 years ago

985a56b1

feat(tactic/explode): support exploding "let" expressions and improve handling of "have" expressions (#3632)

minchaowu committed 5 years ago

1a393e7a

feat(geometry): first stab on Lie groups (#3529)

Nicknamen committed 5 years ago

43ccce55

Newer Older