leanprover-community/mathlib3

Pull Requests Commits

Merge branch 'master' into YK-grigorchuk

urkud committed 2 years ago

dcd7740e

chore(analysis/normed_space/pi_Lp): pi_Lp.equiv is continuous (#18402)

eric-wieser committed 2 years ago

38d38e09

feat (analysis/special_functions): add the Beta function (#18373)

loefflerd committed 2 years ago

c8fc41b2

feat(topology/algebra/infinite_sum): add tsum_finset_bUnion_disjoint (#18350)

eric-wieser committed 2 years ago

cd424234

refactor(topology/discrete_quotient): review API (#18401)

urkud committed 2 years ago

d101e931

feat(combinatorics/simple_graph/ends): Definition (only) of the ends of a simple_graph. (#17857)

bottine committed 2 years ago

db53863f

feat(logic/equiv/fin): `div`/`mod` as an equivalence on `nat`/`int` (#18359)

eric-wieser committed 2 years ago

bd835ef5

feat(combinatorics/catalan): Connection between Catalan numbers and number of trees (#16583)

prakol16 committed 2 years ago

26b40791

feat(analysis/complex/basic): lemmas about tsum (#18376)

eric-wieser committed 2 years ago

2407f3b1

doc(topology/uniform_space/abstract_completion): typo (#18399)

mcdoll committed 2 years ago

69966de7

feat(analysis/calculus/special_functions): refactor bump functions (#17453)

sgouezel committed 2 years ago

b018406a

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

leanprover-community-bot committed 2 years ago

3e32bc90

feat(set_theory/zfc/basic): define `hereditarily` (#18328)

astrainfinita committed 2 years ago

98e83c3d

feat(analysis/convolution): integral of a convolution over positive reals (#18353)

loefflerd committed 2 years ago

50092e4a

chore(topology/noetherian_space): golf (#18394)

urkud committed 2 years ago

0eb49606

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

leanprover-community-bot committed 2 years ago

50832dae

chore: Add toml file for archive and counterexamples (#18388)

eric-wieser committed 2 years ago

2d6f88c2

feat(algebra/big_operators/order): prod_pos lemma for `ennreal` (#18391)

eric-wieser committed 2 years ago

bb37dbda

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

leanprover-community-bot committed 2 years ago

0a0ec350

docs(algebra/module/linear_map): Fix a copy/paste error (#18389)

nomeata committed 2 years ago

cc8e88c7

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

leanprover-community-bot committed 2 years ago

4c19a16e

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

leanprover-community-bot committed 2 years ago

c4bcf3ac

feat(number_theory/number_field/embeddings): add card_complex_embeddings (#17753)

xroblot committed 2 years ago

ff6bde6f

chore(topology/algebra/infinite_sum): add lemmas about division (#18351)

eric-wieser committed 2 years ago

b363547b

feat(ring_theory/ideal/norm): relative ideal norm (#18303)

Vierkantor committed 2 years ago

85e3c05a

refactor(combinatorics/simple_graph/density): Generalize to arbitrary ordered fields (#18370)

YaelDillies committed 2 years ago

a4ec43f5

feat(algebra/order/chebyshev): Special case using division (#18369)

YaelDillies committed 2 years ago

b7399344

chore(100.yaml): Brouwer fix point (#18372)

Vierkantor committed 2 years ago

00ed28cd

refactor(tactic/wlog): simplify and speed up `wlog` (#16495)

jcommelin committed 2 years ago

92ca63f0

chore(topology/algebra/infinite_sum): lemmas about pi.single (#18360)

eric-wieser committed 2 years ago

bed4f052

Older