leanprover-community/mathlib

Pull Requests Commits

eric-wieser committed 2 years ago

98751edf

eric-wieser committed 2 years ago

ea0ba771

finish with the finsupp directory

eric-wieser committed 2 years ago

1186ed53

eric-wieser committed 2 years ago

0dc3a90d

Add decidable arguments to finsupp

eric-wieser committed 2 years ago

18f878dc

doc(order/game_add): improve docstrings (#18269)

vihdzp committed 2 years ago

6f870fad

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

leanprover-community-bot committed 2 years ago

0be37584

refactor(analysis/complex/basic, data/complex/is_R_or_C): downgrade imports (#18217)

hrmacbeth committed 2 years ago

468b141b

feat(linear_algebra/dual): more about dual annihilator, some refactoring, and documentation (#17521)

kmill committed 2 years ago

68626536

feat(algebraic_geometry/elliptic_curve/weierstrass): define a basis for the coordinate ring (#18101)

Multramate committed 2 years ago

808ea4eb

refactor(data/nat/parity): reduce imports, add/delete lemmas (#18221)

urkud committed 2 years ago

8631e2d5

chore(data/finsupp/defs): move lemmas out of the single section which are not about single (#18260)

eric-wieser committed 2 years ago

33694ffd

chore(*): add mathlib4 synchronization comments (#18218)

leanprover-community-bot committed 2 years ago

327c3c0d

fix(*/finsupp/*): add missing decidable arguments in lemma statements (#18251)

eric-wieser committed 2 years ago

6e492fdb

feat(data/tree): Add definitions about binary trees; special support for `tree unit` (#16715)

prakol16 committed 2 years ago

ed989ff5

doc(computability/primrec): remove doc nolints (#16018)

vihdzp committed 2 years ago

959c3b69

chore(field_theory/minpoly/*): replace `gcd_monoid.lean` by `is_integrally_closed.lean` and remove results that have been generalized (#18206)

Paul-Lez committed 2 years ago

2032a878

refactor(data/set/finite): reduce imports (#18245)

urkud committed 2 years ago

1f0096e6

chore(analysis/von_neumann_algebra/basic): add missing API lemmas (#18227)

eric-wieser committed 2 years ago

160ef3e3

feat(special_functions/trigonometric/bounds): Add the inequality `cos x < 1 / sqrt (x ^ 2 + 1)` (#18189)

loefflerd committed 2 years ago

9df54c1b

feat(data/nat/hyperoperation): Defined hyperoperation and added related lemmas (#18116)

Nazgand committed 2 years ago

386c02e7

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

urkud committed 2 years ago

71efed1b

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

urkud committed 2 years ago

fc3dc609

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

eric-wieser committed 2 years ago

ae5357f9

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

vihdzp committed 2 years ago

800d3d45

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

eric-wieser committed 2 years ago

831c4940

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

urkud committed 2 years ago

02315164

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

eric-wieser committed 2 years ago

f2edd790

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

bottine committed 2 years ago

d6fad0e5

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

kmill committed 2 years ago

e1503e02

Older