leanprover-community/mathlib

Pull Requests Commits

lint fixes, rename some dubiously named variables

fpvandoorn committed 5 years ago

8e7e9e73

fixes and docstrings

fpvandoorn committed 5 years ago

21a58c74

broken, in progress

fpvandoorn committed 5 years ago

9b84e22d

start on opposite group

fpvandoorn committed 5 years ago

721124dd

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

ChrisHughes24 committed 5 years ago

3ae6cea5

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

urkud committed 5 years ago

78fe862a

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

jsm28 committed 5 years ago

8f02ad2f

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

urkud committed 5 years ago

14d206b3

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

dupuisf committed 5 years ago

ed377e13

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

urkud committed 5 years ago

b4a6651f

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

urkud committed 5 years ago

b0de8114

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

fpvandoorn committed 5 years ago

d9a6e478

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

leanprover-community-bot committed 5 years ago

acedda0d

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

urkud committed 5 years ago

b215e952

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

urkud committed 5 years ago

234011d0

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

ChrisHughes24 committed 5 years ago

50d1c485

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

fpvandoorn committed 5 years ago

40c6a295

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

TwoFX committed 5 years ago

018309f0

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

ChrisHughes24 committed 5 years ago

6186c694

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

Vierkantor committed 5 years ago

b8df8aac

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

jsm28 committed 5 years ago

5f9e4277

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

urkud committed 5 years ago

aef7ade7

chore(algebra/group_ring_action): docstring, move monoid.End to algebra/group/hom (#3671)

kckennylau committed 5 years ago

c6381aa1

feat(measure_theory/measure_space): add 3 typeclasses (#3664)

urkud committed 5 years ago

b2be1eeb

feat(algebra/category/Group): the category of abelian groups is abelian (#3621)

TwoFX committed 5 years ago

3781435d

feat(analysis/normed_space/real_inner_product): orthogonal projection (#3563)

jsm28 committed 5 years ago

6079ef96

feat(data/finset/lattice,data/finset/sort): singleton lemmas (#3668)

jsm28 committed 5 years ago

8e0d111f

chore(measure_theory/integration): define composition of a `simple_func` and a measurable function (#3667)

urkud committed 5 years ago

61db67de

doc(category_theory): add library note about 'dsimp, simp' pattern (#3659)

kim-em committed 5 years ago

292c921d

feat(group_theory/submonoid/operations): mrange_eq_map (#3673)

ChrisHughes24 committed 5 years ago

3d41e33f

Older