leanprover-community/mathlib

Pull Requests Commits

refactor(analysis/normed_space/real_inner_product): extend normed_space in the definition (#3060)

sgouezel committed 6 years ago

1f16da1b

perf(tactic/linarith): use key/value lists instead of rb_maps to represent linear expressions (#3004)

robertylewis committed 6 years ago

85b8bdcb

chore(order/basic): move unbundled order classes to `rel_classes (#3066)

urkud committed 6 years ago

7f60a62d

feat(tactic/library_search): small improvements (#3037)

kim-em committed 6 years ago

2c97f239

feat(normed_space/dual): (topological) dual of a normed space (#3021)

hrmacbeth committed 6 years ago

a6534db8

chore(data/complex/basic): rearrange into sections (#3068)

bryangingechen committed 6 years ago

4e886875

feat(algebra/continued_fractions): add correctness of terminating computations (#2911)

kappelmann committed 6 years ago

2cd329fe

feat(geometry/euclidean): sum of angles of a triangle (#2994)

jsm28 committed 6 years ago

fdc326c0

refactor(order/basic): make `*order.lift` use `[]` argument (#3067)

urkud committed 6 years ago

c8c18697

doc(measure_theory): document basic measure theory files (#3057)

fpvandoorn committed 6 years ago

67f72889

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

leanprover-community-bot committed 6 years ago

0f98c37c

feat(topology/metric_space/pi_Lp): L^p distance on finite products (#3059)

sgouezel committed 6 years ago

e33245ca

feat(linear_algebra/finite_dimensional): cardinalities and linear independence (#3056)

jcommelin committed 6 years ago

cc16d35b

feat(tactic/linarith): improve parsing expressions into linear form (#2995)

robertylewis committed 6 years ago

b7048a4e

doc(algebra/group/to_additive): add doc strings and tactic doc entry (#3055)

bryangingechen committed 6 years ago

4bb29abb

refactor(topology/uniform_space): docstring and notation (#3052)

PatrickMassot committed 6 years ago

a22b657f

feat(topology/metric_space/pi_lp): Holder and Minkowski inequalities in ennreal (#2988)

sgouezel committed 6 years ago

938b73a4

refactor(ci): only update nolints once a day (#3036)

bryangingechen committed 6 years ago

dc69dc35

feat(linear_algebra): elements of a dim zero space (#3054)

robertylewis committed 6 years ago

1645542c

chore(*): update to Lean 3.16.2c (#3053)

bryangingechen committed 6 years ago

51ad2a18

feat(linear_algebra/affine_space): define a few affine maps (#2981)

urkud committed 6 years ago

ce594be5

feat(data/*): lemmas converting finset, set.finite, and their card (#3042)

pechersky committed 6 years ago

14292790

fix(library_search): only unfold reducible definitions when matching (#3038)

kim-em committed 6 years ago

c955537e

chore(*): remove extra author info (#3051)

pechersky committed 6 years ago

5c0000c0

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

leanprover-community-bot committed 6 years ago

64461b83

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

leanprover-community-bot committed 6 years ago

6aa24643

chore(data/complex/exponential): linting and pp_nodot (#3045)

bryangingechen committed 6 years ago

f78693db

feat(analysis/mean_inequalities): Holder and Minkowski inequalities (#3025)

urkud committed 6 years ago

5808afcb

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

leanprover-community-bot committed 6 years ago

27a09466

chore(data/real/cau_seq): linting (#3040)

bryangingechen committed 6 years ago

30e620ce

Newer Older