leanprover-community/mathlib

Pull Requests Commits

chore(data/matrix/basic): rename _val lemmas to _apply (#3297)

kim-em committed 6 years ago

5fc62815

chore(topology/category/Top/opens): module-doc, cleanup, and construct some morphisms (#3601)

kim-em committed 6 years ago

d952e8bf

chore(ring_theory/ideals): Move the definition of ideals out of algebra/module (#3692)

eric-wieser committed 6 years ago

c63dad10

feat(algebra/*/ulift): algebraic instances for ulift (#3675)

kim-em committed 6 years ago

4a82e849

feat(linear_algebra/affine_space): faces of simplices (#3691)

jsm28 committed 6 years ago

2b9ac697

docs(algebra/module): Remove completed TODO (#3690)

eric-wieser committed 6 years ago

ecb5c5f5

feat(algebra/classical_lie_algebras): add definitions of missing classical Lie algebras (#3661)

Oliver Nash committed 6 years ago

0531cb0c

feat(topology): normed spaces are (locally) path connected (#3689)

PatrickMassot committed 6 years ago

37119b41

refactor(*): add a notation for `nhds_within` (#3683)

urkud committed 6 years ago

545186ca

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

jsm28 committed 6 years ago

3b268785

feat(topology): path connected spaces (#3627)

PatrickMassot committed 6 years ago

84b450d4

feat(data/list/defs): add monadic versions of list.{find,any,all,bor,band} (#3679)

JLimperg committed 6 years ago

f4b2790d

feat(group_theory/submonoid/operations): transfer galois connection/insertion lemmas (#3657)

ChrisHughes24 committed 6 years ago

3ae6cea5

chore(measure_theory/lebesgue_measure): review (#3686)

urkud committed 6 years ago

78fe862a

feat(geometry/euclidean): orthogonal projection (#3662)

jsm28 committed 6 years ago

8f02ad2f

feat(order/filter/interval): define class `filter.is_interval_generated` (#3663)

urkud committed 6 years ago

14d206b3

feat(analysis/convex): a local minimum of a convex function is a global minimum (#3613)

dupuisf committed 6 years ago

ed377e13

chore(order/filter/at_top_bot): golf three proofs (#3684)

urkud committed 6 years ago

b4a6651f

chore(measure_theory/borel_space): DRY by using `order_dual` (#3685)

urkud committed 6 years ago

b0de8114

feat(measure_theory/group): regular, invariant, and conjugate measures (#3650)

fpvandoorn committed 6 years ago

d9a6e478

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

leanprover-community-bot committed 6 years ago

acedda0d

fix(data/set/intervals/basic): fix a typo (#3680)

urkud committed 6 years ago

b215e952

chore(order/filter/lift): prove `has_basis.lift` and `has_basis.lift'` (#3618)

urkud committed 6 years ago

234011d0

feat(order/galois_connection): galois_coinsertions (#3656)

ChrisHughes24 committed 6 years ago

50d1c485

feat(measure_theory/content): define outer measure from content (#3649)

fpvandoorn committed 6 years ago

40c6a295

chore(linear_algebra/basis): replace explicit arguments for 0 ≠ 1 with nontrivial R (#3678)

TwoFX committed 6 years ago

018309f0

feat(group_theory/subgroup): range_gpowers_hom (#3677)

ChrisHughes24 committed 6 years ago

6186c694

feat(algebra/ring): the codomain of a ring hom is trivial iff ... (#3676)

Vierkantor committed 6 years ago

b8df8aac

feat(analysis/normed_space/add_torsor): isometries of normed_add_torsors (#3666)

jsm28 committed 6 years ago

5f9e4277

feat(data/set/intervals): a few lemmas needed by FTC-1 (#3653)

urkud committed 6 years ago

aef7ade7

Newer Older