leanprover-community/mathlib

Pull Requests Commits

refactor(topology/algebra/ordered): rename `tendsto_of_tendsto_of_tendsto_of_le_of_le` to `tendsto_of_tendsto_of_tendsto_of_le_of_le'` (#2111)

urkud committed 6 years ago

Verified d8d09271

refactor(analysis/normed_space/banach): use bundled `→L[𝕜]` maps (#2107)

urkud committed 6 years ago

Verified 4258f5ee

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

434b6299

doc(docs/tutorial/category_theory): introductory category theory tutorial (#2104)

kbuzzard committed 6 years ago

Verified ce7248ab

chore(algebra/group): streamlining imports (#2099)

kim-em committed 6 years ago

Verified 61d70ce8

fix(deprecated/group): remove dangerous instances (#2096)

gebner committed 6 years ago

Verified ca370cb9

chore(category_theory/functor): make arguments implicit (#2103)

kim-em committed 6 years ago

Verified 15d3268e

Remove limits.lean which is superseded by limits_of_products_and_equalizers.lean (#2105)

TwoFX committed 6 years ago

Verified b7444b03

feat(data/fin_enum): `fin_enum` class for finite types with an enumeration order (#1368)

cipher1024 committed 6 years ago

Verified d53bbb6e

feat(lint): add two new linters (#2089)

fpvandoorn committed 6 years ago

Verified 726d83f1

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

c5437b4b

kim-em committed 6 years ago

6cea6d3c

to_additive comes last

kim-em committed 6 years ago

ebc6725a

feat(category_theory): limits and colimits in Ab

kim-em committed 6 years ago

d457ee68

feat(data/set/lattice): add @[simp] to lemmas (#2091)

kim-em committed 6 years ago

Verified 6c23bad2

refactor(group_theory/monoid_localization): use characteristic predicate (#2004)

101damnations committed 6 years ago

Verified 4f10d1eb

limits and colimits in AddCommGroup

kim-em committed 6 years ago

344880eb

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

36b336cb

fix(category_theory/limits): Add some missing instances for special shapes of limits (#2083)

TwoFX committed 6 years ago

Verified 8fb9881a

feat(category_theory/limits): the kernel of the cokernel of an epimorphism is an isomorphism (#2088)

TwoFX committed 6 years ago

Verified f81f861e

feat(data/traversable): improve support for instances for recursive types (#2072)

cipher1024 committed 6 years ago

Verified 0f9751c2

feat(analysis/calculus/specific_functions): smoothness of exp(-1/x) (#2087)

sgouezel committed 6 years ago

Verified 093ac77a

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

50c4adf9

chore(*): switch to lean 3.6.1 (#2064)

mergify[bot] committed 6 years ago

Verified 78ffbae0

refactor(algebra/lie_algebra): lie_algebra should not extend lie_ring (#2084)

mergify[bot] committed 6 years ago

Verified 85351323

fix(congruence): use has_coe_t instead of has_coe (#2086)

mergify[bot] committed 6 years ago

Verified 7d6c4fbe

chore(analysis/normed_space/basic): rename `ne_mem_of_tendsto_norm_at_top` (#2085)

mergify[bot] committed 6 years ago

Verified 9fc675c4

fix(ci): adjust conditions for fixing steps (#2082)

robertylewis committed 6 years ago

Verified f1124087

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

cc4ac8a6

fix(CI/documentation): add a name back

cipher1024 committed 6 years ago

Verified 0f1eb80e

Newer Older