Changelog

2023-02-09 01:31 b6da1a0b
chore(*): add mathlib4 synchronization comments (#18406) …
11 files
2023-02-08 20:27 38d38e09
chore(analysis/normed_space/pi_Lp): pi_Lp.equiv is continuous (#18402) …
1 files4 theorems
2023-02-08 20:27 c8fc41b2
feat (analysis/special_functions): add the Beta function (#18373) …
1 files8 theorems
2023-02-08 20:27 cd424234
feat(topology/algebra/infinite_sum): add tsum_finset_bUnion_disjoint (#18350) …
1 files2 theorems
2023-02-08 18:27 d101e931
refactor(topology/discrete_quotient): review API (#18401) …
3 files51 theorems5 defs1 structures
2023-02-08 18:27 db53863f
feat(combinatorics/simple_graph/ends): Definition (only) of the ends of a simple_graph. (#17857)
4 files27 theorems8 defs
2023-02-08 15:26 bd835ef5
feat(logic/equiv/fin): `div`/`mod` as an equivalence on `nat`/`int` (#18359) …
3 files2 defs
2023-02-08 14:04 26b40791
feat(combinatorics/catalan): Connection between Catalan numbers and number of trees (#16583) …
1 files7 theorems2 defs
2023-02-08 12:29 2407f3b1
feat(analysis/complex/basic): lemmas about tsum (#18376) …
1 files24 theorems
2023-02-08 10:26 69966de7
doc(topology/uniform_space/abstract_completion): typo (#18399)
1 files
2023-02-08 10:26 b018406a
feat(analysis/calculus/special_functions): refactor bump functions (#17453) …
6 files67 theorems3 defs4 structures
2023-02-08 07:36 3e32bc90
chore(*): add mathlib4 synchronization comments (#18398) …
13 files
2023-02-07 20:26 98e83c3d
feat(set_theory/zfc/basic): define `hereditarily` (#18328) …
1 files4 theorems1 defs
2023-02-07 09:01 50092e4a
feat(analysis/convolution): integral of a convolution over positive reals (#18353) …
1 files3 theorems
2023-02-07 07:32 0eb49606
chore(topology/noetherian_space): golf (#18394) …
1 files1 theorems
2023-02-07 04:08 50832dae
chore(*): add mathlib4 synchronization comments (#18393) …
32 files
2023-02-07 01:58 2d6f88c2
chore: Add toml file for archive and counterexamples (#18388) …
16 files182 theorems44 defs6 structures
2023-02-06 23:03 bb37dbda
feat(algebra/big_operators/order): prod_pos lemma for `ennreal` (#18391) …
2 files3 theorems
2023-02-06 06:28 0a0ec350
chore(*): add mathlib4 synchronization comments (#18387) …
18 files
2023-02-05 20:22 cc8e88c7
docs(algebra/module/linear_map): Fix a copy/paste error (#18389)
1 files
2023-02-04 09:12 4c19a16e
chore(*): add mathlib4 synchronization comments (#18381) …
15 files
2023-02-04 03:54 c4bcf3ac
chore(scripts): update nolints.txt (#18385) …
2 files
2023-02-03 21:38 ff6bde6f
feat(number_theory/number_field/embeddings): add card_complex_embeddings (#17753) …
1 files8 theorems
2023-02-03 19:48 b363547b
chore(topology/algebra/infinite_sum): add lemmas about division (#18351) …
2 files7 theorems
2023-02-03 19:48 85e3c05a
feat(ring_theory/ideal/norm): relative ideal norm (#18303) …
2 files18 theorems1 defs
2023-02-03 18:30 a4ec43f5
refactor(combinatorics/simple_graph/density): Generalize to arbitrary ordered fields (#18370) …
1 files
2023-02-03 18:30 b7399344
feat(algebra/order/chebyshev): Special case using division (#18369) …
2 files3 theorems
2023-02-03 13:16 00ed28cd
chore(100.yaml): Brouwer fix point (#18372) …
1 files
2023-02-03 13:16 92ca63f0
refactor(tactic/wlog): simplify and speed up `wlog` (#16495) …
48 files
2023-02-03 11:16 bed4f052
chore(topology/algebra/infinite_sum): lemmas about pi.single (#18360) …
1 files2 theorems
2023-02-03 08:20 0ebfdb71
chore(*): add mathlib4 synchronization comments (#18365) …
19 files
2023-02-03 03:01 84dc0bd6
chore(topology/order/basic): split (#18363) …
11 files11 theorems
2023-02-02 17:00 2705404e
refactor(linear_algebra/basic): extract content about linear_map.general_linear_group (#18345)
9 files4 theorems8 defs
2023-02-02 14:06 8a035e9a
feat(counterexamples/quadratic_form): symmetric bilinear forms in char 2 do not always inject into quadratic forms (#18146)
1 files5 theorems1 defs
2023-02-02 11:40 da1d134a
feat(analysis/special_functions/pow): strengthen cpow integrability lemmas (#18354) …
3 files9 theorems
2023-02-02 10:32 2e59a6de
feat(ring_theory/localization): remove extraneous `algebra_map_submonoid S M ≤ S⁰` conditions (#18358)
3 files4 theorems
2023-02-02 08:56 aebd3428
feat(algebra/order/chebyshev): Chebyshev's Sum Inequality (#13187) …
1 files9 theorems
2023-02-02 06:16 f16e7a22
chore(*): add mathlib4 synchronization comments (#18355) …
18 files
2023-02-02 05:09 4ef778c2
chore(scripts): update nolints.txt (#18357) …
1 files
2023-02-01 20:47 d90e4e18
feat(analysis/special_functions/gaussian): Fourier transform of Gaussian (#18338) …
1 files9 theorems1 defs
2023-02-01 20:47 b3607518
feat(analysis/calculus/bump_function_findim): construct good bump functions on finite-dimensional spaces (#18095) …
2 files25 theorems4 defs1 structures
2023-02-01 19:20 938fead7
fix(algebra/lie/*): use correct terminology for `centralizer` and `normalizer` in Lie theory (#18348) …
5 files25 theorems2 defs
2023-02-01 15:31 6010cf52
feat(ring_theory/dedekind_domain): lemmas for showing Dedekind domains are PIDs (#18301) …
8 files22 theorems1 defs
2023-02-01 12:38 ae690b0c
refactor(linear_algebra/{general,special}_linear_group): move to matrix subfolder (#18344) …
7 files
2023-02-01 12:38 11b92770
feat(linear_algebra/bilinear_form): arithmetic lemmas about symm/refl/alt (#18340) …
2 files9 theorems
2023-02-01 12:38 d7859726
refactor(data/fintype/basic): move fin_choice to a new file (#18337) …
3 files4 theorems4 defs
2023-02-01 09:29 2f4cdce0
feat(linear_algebra/affine_space/basis): `reindex` API (#18190) …
10 files31 theorems2 defs
2023-02-01 07:41 980755c3
feat(analysis/special_functions/trigonometric): Euler's infinite product for sine (part b) (#18281)
2 files10 theorems
2023-02-01 07:41 78ac1db3
feat(number_theory/number_field/embeddings): add infinite_places.eq_iff (#17285) …
2 files8 theorems2 defs
2023-02-01 05:07 e46da4e3
chore(*): add mathlib4 synchronization comments (#18342) …
14 files