Changelog

2023-06-09 01:23 74f1d619
feat(analysis/convex/cone/proper): define proper cone (#18913) …
1 files15 theorems1 defs1 structures
2023-06-08 04:42 7e5137f5
chore(*): add mathlib4 synchronization comments (#19165) …
37 files
2023-06-07 19:34 b915e939
feat(ring_theory/subring): centralizer as a subring (#18861)
7 files22 theorems1 defs
2023-06-07 16:34 31c24aa7
feat(algebra/star/basic): refactor `star_ordered_ring` to include `add_submonoid.closure` (#18854) …
9 files13 theorems3 defs
2023-06-07 13:00 e354e865
feat(geometry/manifold): lemmas from the sphere eversion project (#18877) …
11 files50 theorems3 defs
2023-06-07 11:35 3b92d54a
chore(probability/kernel/composition): redefine kernel.comp using measure.bind, remove kernel.map_measure (#19160) …
2 files21 theorems2 defs
2023-06-07 10:28 0dc40792
refactor(geometry/manifold/cont_mdiff_map): refactor to reduce imports (#19164) …
4 files
2023-06-07 07:55 81843c08
feat (number_theory/zeta_function): func eqn + link to Bernoulli nos (#19158) …
1 files11 theorems
2023-06-07 06:47 6b016921
chore(linear_algebra/eigenspace): split file (#19163)
7 files16 theorems
2023-06-07 05:24 c2092722
chore(*): add mathlib4 synchronization comments (#19162) …
38 files
2023-06-06 17:18 58a27226
chore(algebra/algebra/spectrum): split file (#19161) …
5 files16 theorems
2023-06-06 05:16 36938f77
chore(*): add mathlib4 synchronization comments (#19159) …
48 files
2023-06-05 08:24 a3209ddf
feat (special_functions/gamma): doubling formula (#19136) …
4 files18 theorems1 defs
2023-06-05 06:26 575b4ea3
chore(*): add mathlib4 synchronization comments (#19157) …
10 files
2023-06-05 06:26 4c3e1721
feat(topology/homotopy/homotopy_group): `group` and `comm_group` instances for `π_n` (#15681) …
3 files33 theorems33 defs1 structures
2023-06-05 05:15 df76f433
chore(field_theory/splitting_field): split file (#19154) …
8 files10 theorems2 defs
2023-06-05 02:20 30882647
chore(archive/imo): fix some naming inconsistencies and whitespace (#19155) …
18 files9 theorems
2023-06-05 01:10 533f62f4
chore(algebraic_geometry/open_immersion): split (#19149) …
6 files60 theorems38 defs
2023-06-04 16:20 13361559
chore(topology/sheaves/*): universe generalizations (#19153) …
12 files8 theorems16 defs
2023-06-04 11:07 5f25c089
chore(archive/imo): change namespace `imo` to `imoYYYY_qX` (#19152) …
27 files298 theorems54 defs2 structures
2023-06-04 05:46 5c1efce1
chore(*): add mathlib4 synchronization comments (#19151) …
19 files
2023-06-03 13:39 af471b9e
chore(*): add mathlib4 synchronization comments (#19148) …
39 files
2023-06-02 16:27 7fdeecc0
chore(ring_theory/root_of_unity): move and split a file (#19144) …
8 files24 theorems
2023-06-02 14:50 3d5c4a7a
feat(measure_theory/measure/hausdorff): invariance instances (#19145) …
1 files
2023-06-02 12:04 571e13ca
feat(measure_theory/measure/hausdorff): the 1-measure of a segment is its length (#18981) …
2 files11 theorems
2023-06-02 09:01 69b2e97a
chore(ring_theory/tensor_product): replace `is_scalar_tower` by `smul_comm_class` in `left_algebra` (#19118) …
1 files1 theorems
2023-06-02 05:41 2ebc1d6c
chore(*): add mathlib4 synchronization comments (#19141) …
18 files
2023-06-02 05:41 a1666563
chore(analysis/convex/specific_functions/deriv): remove unnecessary imports (#19140) …
2 files
2023-06-02 04:32 6a5c8500
chore(analysis/special_functions/exp_deriv): downgrade import (#19139) …
2 files2 theorems
2023-06-01 20:20 34ebaffc
feat(number_theory/sum_two_squares): add result for general n (#19054) …
1 files13 theorems
2023-06-01 19:12 b608348f
chore(ring_theory/derivation): split file (#19138) …
7 files10 theorems8 defs
2023-06-01 16:18 d35b4ff4
chore(ring_theory): remove `splitting_field` dependency from `is_integrally_closed` (#19137) …
2 files4 theorems
2023-06-01 13:20 9d013ad8
doc(analysis/normed_space/pi_Lp): fix corrupt synchronization header (#19134) …
1 files
2023-06-01 08:55 67237461
chore(field_theory/ratfunc): use `section` instead of `omit/include` (#19133) …
1 files1 structures
2023-06-01 06:32 599fffe7
chore(*): add mathlib4 synchronization comments (#19135) …
11 files
2023-06-01 05:11 04e80bb7
refactor(number_theory/liouville/liouville_number): review API, golf (#19126) …
3 files19 theorems6 defs
2023-05-31 19:23 cca40788
feat (number_theory/zeta_function): relate to Dirichlet series (#19131) …
3 files8 theorems1 defs
2023-05-31 13:56 e137999b
feat(analysis/schwartz_space): Multiplication of Schwartz function and functions of temperate growth (#18649)
1 files1 theorems3 defs
2023-05-31 12:41 00abe069
feat(probability/kernel/cond_distrib): regular conditional probability distributions (#19090) …
5 files45 theorems2 defs
2023-05-31 09:30 a99f8522
feat(linear_algebra/matrix/adjugate): add `det_eq_sum_mul_adjugate_row` (#19117) …
2 files5 theorems
2023-05-31 08:02 61b5e275
chore(*): add mathlib4 synchronization comments (#19132) …
22 files
2023-05-31 00:27 12a85fac
chore(field_theory/finite/basic): move a lemma (#19130) …
2 files
2023-05-30 23:18 32837559
chore(archive + counterexamples): namespaces imo, theorems_100, counterexample, plus three more (#19129) …
54 files812 theorems160 defs8 structures4 inductives
2023-05-30 18:50 48dc6abe
feat(linear_algebra/matrix/charpoly/eigs): det and trace are product and sum of eigenvalues (#19079) …
1 files4 theorems
2023-05-30 17:46 938d3db9
feat(ring_theory/polynomial/hermite): proof of explicit formula for Hermite polynomial coefficients (#19044) …
1 files3 theorems
2023-05-30 14:04 74c2af38
feat(data/set/ncard): noncomputable set cardinality (#18576) …
1 files92 theorems
2023-05-30 10:24 9a1ffe49
refactor(analysis/calculus/darboux): review API (#19125) …
1 files11 theorems
2023-05-30 08:50 f60c6087
chore(*): add mathlib4 synchronization comments (#19115) …
42 files
2023-05-30 03:49 bd654783
chore(linear_algebra/alternating): make `ι` an explicit arg of `alternating_map.const_of_is_empty` (#19123) …
3 files1 theorems
2023-05-29 17:56 837f72de
chore(analysis/normed/group/add_torsor): nnnorm lemmas (#18997) …
2 files21 theorems