Commits leanprover-community/mathlib3

chore(field_theory/ratfunc): use `section` instead of `omit/include` (#19133)

adomani committed 2 years ago

67237461

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

github-actions[bot] committed 2 years ago

599fffe7

refactor(number_theory/liouville/liouville_number): review API, golf (#19126)

urkud committed 2 years ago

04e80bb7

feat (number_theory/zeta_function): relate to Dirichlet series (#19131)

loefflerd committed 2 years ago

cca40788

feat(analysis/schwartz_space): Multiplication of Schwartz function and functions of temperate growth (#18649)

mcdoll committed 2 years ago

e137999b

feat(probability/kernel/cond_distrib): regular conditional probability distributions (#19090)

RemyDegenne committed 2 years ago

00abe069

feat(linear_algebra/matrix/adjugate): add `det_eq_sum_mul_adjugate_row` (#19117)

eric-wieser committed 2 years ago

a99f8522

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

github-actions[bot] committed 2 years ago

61b5e275

chore(field_theory/finite/basic): move a lemma (#19130)

riccardobrasca committed 2 years ago

12a85fac

chore(archive + counterexamples): namespaces imo, theorems_100, counterexample, plus three more (#19129)

adomani committed 2 years ago

32837559

feat(linear_algebra/matrix/charpoly/eigs): det and trace are product and sum of eigenvalues (#19079)

MohanadAhmed committed 2 years ago

48dc6abe

feat(ring_theory/polynomial/hermite): proof of explicit formula for Hermite polynomial coefficients (#19044)

jakelev committed 2 years ago

938d3db9

feat(data/set/ncard): noncomputable set cardinality (#18576)

apnelson1 committed 2 years ago

74c2af38

refactor(analysis/calculus/darboux): review API (#19125)

urkud committed 2 years ago

9a1ffe49

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

github-actions[bot] committed 2 years ago

f60c6087

chore(linear_algebra/alternating): make `ι` an explicit arg of `alternating_map.const_of_is_empty` (#19123)

urkud committed 2 years ago

bd654783

chore(analysis/normed/group/add_torsor): nnnorm lemmas (#18997)

eric-wieser committed 2 years ago

837f72de

doc(topology/homotopy/H-spaces): add doc about H-spaces. (#19075)

faenuccio committed 2 years ago

729d23f9

feat (number_theory/zeta_function): define zeta (#19027)

loefflerd committed 2 years ago

a8410892

feat(analysis/schwartz_space): partial derivatives (#18755)

mcdoll committed 2 years ago

e3e30a5c

feat(analysis/normed_space/triv_sq_zero_ext): generalize some results to non-commutativity (#19049)

eric-wieser committed 2 years ago

88a563b1

fix(scripts): Allow special character in file names (#11001)

eric-wieser committed 2 years ago

7bf0850d

chore(ring_theory/adjoin_root): modify `field` instance on `adjoin_root` (#19119)

adomani committed 2 years ago

5c4b3d41

refactor(topology/vector_bundle/hom): fibres of hom-bundle carry strong topology (#19107)

hrmacbeth committed 2 years ago

f7ebde7e

feat(linear_algebra/free_module/ideal_quotient): add ideal.finrank_quotient_eq_sum (#19084)

Multramate committed 2 years ago

d87199d5

feat(ring_theory/polynomial/quotient): generalise quotient_span_X_sub_C_alg_equiv (#19086)

Multramate committed 2 years ago

4f840b8d

feat (analysis/mellin_transform): API for mellin transforms (#19110)

loefflerd committed 2 years ago

917c3c07

chore(analysis/calculus/deriv): split file (#19113)

urkud committed 2 years ago

3bce8d80

feat(measure_theory/function/l1_space): generalize multiplicative results to is_unit (#19073)

eric-wieser committed 2 years ago

13b0d72f

chore(measure_theory/function/simple_func_dense_lp): generalize typeclasses (#19111)

eric-wieser committed 2 years ago

5a2df4cd