leanprover-community/mathlib

Pull Requests Commits

fix(order/filter/basic): fix a diamond (#18255)

urkud committed 3 years ago

71efed1b

chore(order/filter/basic): fix 2 typos (#18253)

urkud committed 3 years ago

fc3dc609

refactor(data/finsupp/basic): split out alist results (#18250)

eric-wieser committed 3 years ago

ae5357f9

feat(set_theory/zfc/basic): better docs on `univ_not_mem_univ` (#18234)

vihdzp committed 3 years ago

800d3d45

refactor(group_theory/monoid_localization): flip the direction of multiplication (#15584)

eric-wieser committed 3 years ago

831c4940

refactor(order/filter/basic): drop a lemma (#18254)

urkud committed 3 years ago

02315164

fix(linear_algebra/basis): add missing decidable arguments in lemmas (#18252)

eric-wieser committed 3 years ago

f2edd790

feat(analysis/bounded_variation): define `variation_on_from_to` (#18040)

bottine committed 3 years ago

d6fad0e5

feat(data/sym/sym2): `set_like` instance (#17154)

kmill committed 3 years ago

e1503e02

feat(algebra/group/inj_surj): Missing transfer instances (#18247)

YaelDillies committed 3 years ago

d23418e0

refactor(set_theory/ordinal/arithmetic): fix `rank` universes (#18239)

vihdzp committed 3 years ago

2751ae21

feat(topology/order/lower_topology): Introduce the lower topology on a preorder (#17426)

mans0954 committed 3 years ago

38fe3f3c

chore(group_theory/subgroup/basic): split out finiteness (#18242)

Ruben-VandeVelde committed 3 years ago

6f9f3636

chore(analysis/convex/topology): split (#18187)

hrmacbeth committed 3 years ago

a63928c3

feat(linear_algebra/dual): lemmas (#18228)

themathqueen committed 3 years ago

2d3f0c84

fix(data/finsupp/basic): add missing `decidable` arguments in lemma statements (#18241)

eric-wieser committed 3 years ago

2445c98a

feat(data/finset/basic): `finset.to_list_eq_singleton_iff` (#18236)

vihdzp committed 3 years ago

68cc4218

feat(special_functions/gamma): Bohr-Mollerup theorem (#18188)

loefflerd committed 3 years ago

52e2fbbd

chore(*): detect blobs in port_status (#18237)

mo271 committed 3 years ago

3f0c8b32

feat(data/list/alist): recursion on `alist` using `insert` (#15434)

vihdzp committed 3 years ago

f808feb6

chore(group_theory/subgroup/basic): split out some self-contained sections (#17862)

Ruben-VandeVelde committed 3 years ago

0f6670b8

fix(topology/basic): docstring typo (#18229)

rwbarton committed 3 years ago

1126441d

feat(algebra/group/basic): reduce additivity checks to one case (#18080)

alreadydone committed 3 years ago

4060545f

chore(data/fintype/vector, logic/equiv/list): split (#18226)

eric-wieser committed 3 years ago

78314d08

chore(data/nat/digits): golf, use seemingly weaker assumptions (#18203)

urkud committed 3 years ago

2609ad04

feat(analysis/special_functions/pow): interaction between `cpow` and `inv`/`conj` (#18137)

eric-wieser committed 3 years ago

9292ecc2

chore(analysis/complex/cauchy_integral): squeeze simp (#18225)

eric-wieser committed 3 years ago

e94cd75f

feat(topology/algebra/infinite_sum): Generalized lemmas for `add_comm_monoid` rather than `add_comm_group` (#17035)

dtumad committed 3 years ago

b84da9c8

refactor(analysis/normed/group/hom): split (#18219)

hrmacbeth committed 3 years ago

3c422528

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

leanprover-community-bot committed 3 years ago

1684fd2a

Newer Older