leanprover-community/mathlib

Pull Requests Commits

bottine committed 2 years ago

d7ad1424

was wrong, just need to swap args

bottine committed 2 years ago

86b33556

destutter preserves list.edist needs induction over the length of the list, since the cases we induct over are not structural sublists

bottine committed 2 years ago

c851e4e3

bottine committed 2 years ago

2433c7cb

bottine committed 2 years ago

c226f279

Just to have it out

bottine committed 2 years ago

ff8fb537

bottine committed 2 years ago

890e557f

bottine committed 2 years ago

ca8e91ca

bottine committed 2 years ago

f2073d18

bottine committed 2 years ago

aec122b3

bottine committed 2 years ago

7cfcff17

bottine committed 2 years ago

0f1477ab

bottine committed 2 years ago

ed2042b8

making good progress imo

bottine committed 2 years ago

8da189a6

init. The goal is to rewrite all of bounded_variation using lists (or maybe finsets)

bottine committed 2 years ago

3b90244c

feat(topology/instances/add_circle): expand API for finite-order points on the circle (#17986)

ocfnash committed 2 years ago

422e70f7

feat(*): bump to lean 3.50.3 (#18016)

gebner committed 2 years ago

46a64b5b

perf(analysis/inner_product_space/basic): speedups (#18018)

alreadydone committed 2 years ago

79ceafba

feat(order/locally_finite): `finset.interval` (#17939)

YaelDillies committed 2 years ago

a7b92725

feat(analysis/complex/locally_uniform_limit): compact limits of holomorphic fns are holomorphic (#17074)

vbeffara committed 2 years ago

839ab10c

feat(analysis/bounded_variation): `evariation_on` of precomposition with monotone/antitone map. (#18001)

bottine committed 2 years ago

cd9a9326

feat(analysis/complex): integration and differentiation `ℝ → ℂ` (#17989)

loefflerd committed 2 years ago

e9be2fa7

feat(algebra/geom_sum): divisibility of sums and differences of powers (#17996)

nielsvoss committed 2 years ago

8acf2263

feat(algebra/cubic_discriminant): extract useful lemma from eq_sum_three_roots (#17999)

Multramate committed 2 years ago

93013316

feat(analysis/normed_space/affine_isometry, linear_algebra/affine_space/affine_equiv): restrict affine isometry to isometry equivalence (#17522)

datokrat committed 2 years ago

09258fb7

feat(*): bump to lean 3.50.2 (#18007)

gebner committed 2 years ago

717c1321

feat(analysis/locally_convex/bounded): characterize boundedness using sequences (#17688)

ADedecker committed 2 years ago

ac1e2e08

chore(data/nat/modeq): split out lemmas about lists (#18004)

hrmacbeth committed 2 years ago

3813d4ea

chore(*): fix docs and a name generated by to_additive (#18002)

alreadydone committed 2 years ago

cfa57f46

feat(number_theory/number_field/embeddings) : add infinite_places (#17844)

xroblot committed 2 years ago

51c6beb4

Older