leanprover-community/mathlib

Pull Requests Commits

Merge remote-tracking branch 'origin/master' into fpvandoorn/mfderiv

fpvandoorn committed 2 years ago

6ed8f483

feat(set_theory/zfc/basic): more trivial results (#18294)

vihdzp committed 2 years ago

fedcb65c

feat(analysis/special_functions/trigonometric): Euler's infinite product for sine (part a) (#18282)

loefflerd committed 2 years ago

a1ddb551

chore(ring_theory): protect `algebra.is_integral` (#18178)

alreadydone committed 2 years ago

825edd3c

feat(data/list/lemmas): Range of `foldr` (#13328)

vihdzp committed 2 years ago

975c8c32

feat(number_theory/kummer_dedekind): the return of the Dedekind-Kummer theorem. (#16870)

Paul-Lez committed 2 years ago

f7fc89d5

feat(set_theory/zfc/basic): `pSet.equiv.comm` (#18297)

vihdzp committed 2 years ago

cd45082b

feat(data/real/pi): refactor Wallis formula for pi (#18280)

loefflerd committed 2 years ago

9b94375a

feat(special_functions/integrals): integral of `cos(a * x)` for `a` complex (#18279)

loefflerd committed 2 years ago

2ef3da38

chore(set_theory/zfc/basic): `mem_empty` → `not_mem_empty` (#18262)

vihdzp committed 2 years ago

7a1cc03e

feat(algebra/homology/opposite): add opposite complexes (#18144)

Amelia Livingston committed 2 years ago

8c75ef35

chore(set_theory/game/nim): golf `grundy_value_nim_add_nim` (#15878)

vihdzp committed 2 years ago

397a33d9

feat(analysis/special_functions/gamma): monotonicity of the Gamma function (#18246)

loefflerd committed 2 years ago

0ee3e6f5

refactor(number_theory/primorial): split the proof, golf it (#18238)

urkud committed 2 years ago

966e0cf0

feat(geometry/manifold/mfderiv): more arithmetic (#17793)

fpvandoorn committed 2 years ago

f93c1193

feat(analysis/calculus/cont_diff): Prove that `fderiv_within` is `C^n` for functions with parameters (#16946)

fpvandoorn committed 2 years ago

27f315c5

feat(set_theory/zfc/basic): more basic simp/ext lemmas (#18233)

vihdzp committed 2 years ago

996b0ff9

feat(analysis/constant_speed): define constant speed functions and prove existence of the arc-length reparameterization (#18208)

bottine committed 2 years ago

168eeff2

feat(algebra/order/kleene) : Kleene algebras (#17965)

Siddhartha Prasad committed 2 years ago

a239cd3e

feat(order/game_add): add more lemmas (#16082)

vihdzp committed 2 years ago

4d756328

feat(measure_theory/integrals): better interval_integral_pos (#18278)

loefflerd committed 2 years ago

9ac58f08

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

Older