leanprover-community/mathlib

Pull Requests Commits

feat(ring_theory/dedekind_domain): localizing a Dedekind domain at a prime gives DVR (#18264)

Vierkantor committed 2 years ago

926daa81

feat(data/pequiv,order/initial_seg): use `fun_like`, `embedding_like` (#18198)

urkud committed 2 years ago

7c3269ca

feat(data/nat/with_bot): `n < m → n + 1 ≤ m` (#18174)

alreadydone committed 2 years ago

12665d36

feat(algebra/order/ring/with_top): ring covariance & ordered ring typeclasses for `with_bot` (#18149)

astrainfinita committed 2 years ago

e7e2ba8a

chore(*): golf (#18111)

urkud committed 2 years ago

f974ae84

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

leanprover-community-bot committed 2 years ago

4d392a6c

refactor(topology): move `pcontinuous` etc to a new file (#18288)

urkud committed 2 years ago

2987594a

fix(*): add missing `classical` tactics and `decidable` arguments (#18277)

eric-wieser committed 2 years ago

6623e6af

feat(topology/algebra): add converse to tendsto.mul (#18276)

loefflerd committed 2 years ago

a81201cc

chore(test/gmonoid): Add a test of the gmonoid API (#18197)

eric-wieser committed 2 years ago

bbd198e1

feat(tactic/simps): store generated lemmas in attribute (#17964)

fpvandoorn committed 2 years ago

e3d9ab8f

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

leanprover-community-bot committed 2 years ago

63f84d91

feat(ring_theory/localization): localization of a basis, again (#18261)

Vierkantor committed 2 years ago

b69c9a77

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

Newer Older